src/FOL/cladata.ML
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 32261 05e687ddbcee
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     1
(*  Title:      FOL/cladata.ML
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     2
    Author:     Tobias Nipkow
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     3
    Copyright   1996  University of Cambridge
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     4
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 7156
diff changeset
     5
Setting up the classical reasoner.
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     6
*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     7
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     8
(*** Applying ClassicalFun to create a classical prover ***)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
     9
structure Classical_Data = 
26411
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26287
diff changeset
    10
struct
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26287
diff changeset
    11
  val imp_elim  = @{thm imp_elim}
26287
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    12
  val not_elim  = @{thm notE}
26411
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26287
diff changeset
    13
  val swap      = @{thm swap}
26287
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    14
  val classical = @{thm classical}
9158
084abf3d0eff declaring and using cla_make_elim
paulson
parents: 8099
diff changeset
    15
  val sizef     = size_of_thm
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    16
  val hyp_subst_tacs=[hyp_subst_tac]
26411
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26287
diff changeset
    17
end;
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    18
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    19
structure Cla = ClassicalFun(Classical_Data);
8099
6a087be9f6d9 ObtainFun;
wenzelm
parents: 7355
diff changeset
    20
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    21
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31974
diff changeset
    22
ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 7156
diff changeset
    23
2844
05d78159812d Now uses the alternative (safe!) rules for ex1
paulson
parents: 2469
diff changeset
    24
4305
03d7de40ee4f The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents: 4095
diff changeset
    25
(*Propositional rules*)
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 18708
diff changeset
    26
val prop_cs = empty_cs
26287
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    27
  addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    28
    @{thm notI}, @{thm iffI}]
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    29
  addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    30
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    31
(*Quantifier rules*)
26287
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    32
val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
df8e5362cff9 proper antiquotations;
wenzelm
parents: 22127
diff changeset
    33
                     addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents:
diff changeset
    34