author | wenzelm |
Mon, 05 May 2008 15:23:59 +0200 | |
changeset 26783 | 1651ff6a34b5 |
parent 26496 | 49ae9456eba9 |
child 27211 | 6724f31a1c8e |
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 |
||
11 |
(*** Applying ClassicalFun to create a classical prover ***) |
|
12 |
structure Classical_Data = |
|
26411 | 13 |
struct |
14 |
val imp_elim = @{thm imp_elim} |
|
26287 | 15 |
val not_elim = @{thm notE} |
26411 | 16 |
val swap = @{thm swap} |
26287 | 17 |
val classical = @{thm classical} |
9158 | 18 |
val sizef = size_of_thm |
2469 | 19 |
val hyp_subst_tacs=[hyp_subst_tac] |
26411 | 20 |
end; |
2469 | 21 |
|
22 |
structure Cla = ClassicalFun(Classical_Data); |
|
8099 | 23 |
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
2469 | 24 |
|
22127 | 25 |
ML_Context.value_antiq "claset" |
26 |
(Scan.succeed ("claset", "Cla.local_claset_of (ML_Context.the_local_context ())")); |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
7156
diff
changeset
|
27 |
|
2844 | 28 |
|
4305
03d7de40ee4f
The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents:
4095
diff
changeset
|
29 |
(*Propositional rules*) |
21539 | 30 |
val prop_cs = empty_cs |
26287 | 31 |
addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI}, |
32 |
@{thm notI}, @{thm iffI}] |
|
33 |
addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}]; |
|
2469 | 34 |
|
35 |
(*Quantifier rules*) |
|
26287 | 36 |
val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] |
37 |
addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; |
|
2469 | 38 |
|
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26411
diff
changeset
|
39 |
val cla_setup = Cla.map_claset (K FOL_cs); |
14156 | 40 |
|
41 |
val case_setup = |
|
18708 | 42 |
(Method.add_methods |
14156 | 43 |
[("case_tac", Method.goal_args Args.name case_tac, |
18708 | 44 |
"case_tac emulation (dynamic instantiation!)")]); |