isabelle: src/FOL/cladata.ML@4a71cc58b203 (annotated)

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	ID: $Id$
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	3	Author: Tobias Nipkow
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	4	Copyright 1996 University of Cambridge
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	5
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 7156 diff changeset	6	Setting up the classical reasoner.
2469 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
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	9	(* Applying ClassicalFun to create a classical prover *)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	10	structure Classical_Data =
26411 cd74690f3bfb pass imp_elim, swap to classical prover; wenzelm parents: 26287 diff changeset	11	struct
cd74690f3bfb pass imp_elim, swap to classical prover; wenzelm parents: 26287 diff changeset	12	val imp_elim = @{thm imp_elim}
26287 df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	13	val not_elim = @{thm notE}
26411 cd74690f3bfb pass imp_elim, swap to classical prover; wenzelm parents: 26287 diff changeset	14	val swap = @{thm swap}
26287 df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	15	val classical = @{thm classical}
9158 084abf3d0eff declaring and using cla_make_elim paulson parents: 8099 diff changeset	16	val sizef = size_of_thm
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	17	val hyp_subst_tacs=[hyp_subst_tac]
26411 cd74690f3bfb pass imp_elim, swap to classical prover; wenzelm parents: 26287 diff changeset	18	end;
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	19
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	20	structure Cla = ClassicalFun(Classical_Data);
8099 6a087be9f6d9 ObtainFun; wenzelm parents: 7355 diff changeset	21	structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	22
27338 2cd6c60cc10b ML_Antiquote.value; wenzelm parents: 27211 diff changeset	23	ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())");
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 7156 diff changeset	24
2844 05d78159812d Now uses the alternative (safe!) rules for ex1 paulson parents: 2469 diff changeset	25
4305 03d7de40ee4f The change from iffE to iffCE means fewer case splits in most cases. Very few paulson parents: 4095 diff changeset	26	(Propositional rules)
21539 c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 18708 diff changeset	27	val prop_cs = empty_cs
26287 df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	28	addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	29	@{thm notI}, @{thm iffI}]
df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	30	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	31
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	32	(Quantifier rules)
26287 df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	33	val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
df8e5362cff9 proper antiquotations; wenzelm parents: 22127 diff changeset	34	addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: diff changeset	35
26496 49ae9456eba9 purely functional setup of claset/simpset/clasimpset; wenzelm parents: 26411 diff changeset	36	val cla_setup = Cla.map_claset (K FOL_cs);

author	haftmann
	Mon, 10 Nov 2008 08:18:57 +0100
changeset 28725	4a71cc58b203
parent 27849	c74905423895
child 31974	e81979a703a4
permissions	-rw-r--r--