--- a/src/FOL/simpdata.ML Sun Nov 26 23:09:25 2006 +0100
+++ b/src/FOL/simpdata.ML Sun Nov 26 23:43:53 2006 +0100
@@ -6,16 +6,11 @@
Simplification data for FOL.
*)
-val ex1_functional = thm "ex1_functional";
-val True_implies_equals = thm "True_implies_equals";
-
-
-
(*** Rewrite rules ***)
fun int_prove_fun s =
(writeln s;
- prove_goal IFOL.thy s
+ prove_goal (theory "IFOL") s
(fn prems => [ (cut_facts_tac prems 1),
(IntPr.fast_tac 1) ]));
@@ -88,7 +83,7 @@
(*Replace premises x=y, X<->Y by X==Y*)
val mk_meta_prems =
rule_by_tactic
- (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
+ (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, thm "def_imp_iff"]));
(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
@@ -169,7 +164,7 @@
(*** Named rewrite rules proved for IFOL ***)
-fun int_prove nm thm = qed_goal nm IFOL.thy thm
+fun int_prove nm thm = qed_goal nm (theory "IFOL") thm
(fn prems => [ (cut_facts_tac prems 1),
(IntPr.fast_tac 1) ]);
@@ -213,23 +208,6 @@
"(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
-local
-val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
- (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
-
-val iff_allI = allI RS
- prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
- (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
-val iff_exI = allI RS
- prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (EX x. P(x)) <-> (EX x. Q(x))"
- (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
-
-val all_comm = prove_goal (the_context()) "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"
- (fn _ => [Blast_tac 1])
-val ex_comm = prove_goal (the_context()) "(EX x y. P(x,y)) <-> (EX y x. P(x,y))"
- (fn _ => [Blast_tac 1])
-in
-
(** make simplification procedures for quantifier elimination **)
structure Quantifier1 = Quantifier1Fun(
struct
@@ -250,17 +228,15 @@
val conjE= conjE
val impI = impI
val mp = mp
- val uncurry = uncurry
+ val uncurry = thm "uncurry"
val exI = exI
val exE = exE
- val iff_allI = iff_allI
- val iff_exI = iff_exI
- val all_comm = all_comm
- val ex_comm = ex_comm
+ val iff_allI = thm "iff_allI"
+ val iff_exI = thm "iff_exI"
+ val all_comm = thm "all_comm"
+ val ex_comm = thm "ex_comm"
end);
-end;
-
val defEX_regroup =
Simplifier.simproc (the_context ())
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
@@ -272,9 +248,6 @@
(*** Case splitting ***)
-bind_thm ("meta_eq_to_iff", prove_goal IFOL.thy "x==y ==> x<->y"
- (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]));
-
structure SplitterData =
struct
structure Simplifier = Simplifier
@@ -284,9 +257,9 @@
val disjE = disjE
val conjE = conjE
val exE = exE
- val contrapos = contrapos
- val contrapos2 = contrapos2
- val notnotD = notnotD
+ val contrapos = thm "contrapos"
+ val contrapos2 = thm "contrapos2"
+ val notnotD = thm "notnotD"
end;
structure Splitter = SplitterFun(SplitterData);
@@ -302,21 +275,22 @@
(*** Standard simpsets ***)
-structure Induction = InductionFun(struct val spec=IFOL.spec end);
+structure Induction = InductionFun(struct val spec = spec end);
open Induction;
bind_thms ("meta_simps",
[triv_forall_equality, (* prunes params *)
- True_implies_equals]); (* prune asms `True' *)
+ thm "True_implies_equals"]); (* prune asms `True' *)
bind_thms ("IFOL_simps",
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
imp_simps @ iff_simps @ quant_simps);
bind_thm ("notFalseI", int_prove_fun "~False");
-bind_thms ("triv_rls", [TrueI,refl,reflexive_thm,iff_refl,notFalseI]);
+bind_thms ("triv_rls",
+ [TrueI, refl, reflexive_thm, iff_refl, thm "notFalseI"]);
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
atac, etac FalseE];
@@ -339,10 +313,11 @@
(*intuitionistic simprules only*)
-val IFOL_ss = FOL_basic_ss
+val IFOL_ss =
+ FOL_basic_ss
addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)
addsimprocs [defALL_regroup, defEX_regroup]
- addcongs [imp_cong];
+ addcongs [thm "imp_cong"];
bind_thms ("cla_simps",
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,