equal
deleted
inserted
replaced
1 (* Title: FOL/cladata.ML |
|
2 Author: Tobias Nipkow |
|
3 Copyright 1996 University of Cambridge |
|
4 |
|
5 Setting up the classical reasoner. |
|
6 *) |
|
7 |
|
8 (*** Applying ClassicalFun to create a classical prover ***) |
|
9 structure Classical_Data = |
|
10 struct |
|
11 val imp_elim = @{thm imp_elim} |
|
12 val not_elim = @{thm notE} |
|
13 val swap = @{thm swap} |
|
14 val classical = @{thm classical} |
|
15 val sizef = size_of_thm |
|
16 val hyp_subst_tacs=[hyp_subst_tac] |
|
17 end; |
|
18 |
|
19 structure Cla = ClassicalFun(Classical_Data); |
|
20 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
|
21 |
|
22 ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())"); |
|
23 |
|
24 |
|
25 (*Propositional rules*) |
|
26 val prop_cs = empty_cs |
|
27 addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI}, |
|
28 @{thm notI}, @{thm iffI}] |
|
29 addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}]; |
|
30 |
|
31 (*Quantifier rules*) |
|
32 val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] |
|
33 addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; |
|
34 |
|