isabelle: src/FOL/cladata.ML@e81979a703a4 (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	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
27338 2cd6c60cc10b ML_Antiquote.value; wenzelm parents: 27211 diff changeset	22	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	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
26496 49ae9456eba9 purely functional setup of claset/simpset/clasimpset; wenzelm parents: 26411 diff changeset	35	val cla_setup = Cla.map_claset (K FOL_cs);

author	wenzelm
	Thu, 09 Jul 2009 22:09:58 +0200
changeset 31974	e81979a703a4
parent 27849	c74905423895
child 32149	ef59550a55d3
permissions	-rw-r--r--