author wenzelm Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago) changeset 18708 4b3dadb4fe33 parent 18529 540da2415751 child 21539 c5cf9243ad62 permissions -rw-r--r--
setup: theory -> theory;
```     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 section "Classical Reasoner";
```
```    10
```
```    11 (*** Applying ClassicalFun to create a classical prover ***)
```
```    12 structure Classical_Data =
```
```    13   struct
```
```    14   val mp        = mp
```
```    15   val not_elim  = notE
```
```    16   val classical = classical
```
```    17   val sizef     = size_of_thm
```
```    18   val hyp_subst_tacs=[hyp_subst_tac]
```
```    19   end;
```
```    20
```
```    21 structure Cla = ClassicalFun(Classical_Data);
```
```    22 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
```
```    23
```
```    24
```
```    25 (*Better for fast_tac: needs no quantifier duplication!*)
```
```    26 qed_goal "alt_ex1E" IFOL.thy
```
```    27     "[| EX! x. P(x);                                              \
```
```    28 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
```
```    29 \    |] ==> R"
```
```    30  (fn major::prems =>
```
```    31   [ (rtac (major RS ex1E) 1),
```
```    32     (REPEAT (ares_tac (allI::prems) 1)),
```
```    33     (etac (dup_elim allE) 1),
```
```    34     (IntPr.fast_tac 1)]);
```
```    35
```
```    36
```
```    37 (*Propositional rules*)
```
```    38 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
```
```    39                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
```
```    40
```
```    41 (*Quantifier rules*)
```
```    42 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
```
```    43                      addSEs [exE,alt_ex1E] addEs [allE];
```
```    44
```
```    45 val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
```
```    46
```
```    47 val case_setup =
```
```    48  (Method.add_methods
```
```    49     [("case_tac", Method.goal_args Args.name case_tac,
```
```    50       "case_tac emulation (dynamic instantiation!)")]);
```