--- a/src/HOL/simpdata.ML Wed Aug 12 16:20:49 1998 +0200
+++ b/src/HOL/simpdata.ML Wed Aug 12 16:21:18 1998 +0200
@@ -3,7 +3,7 @@
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
-Instantiation of the generic simplifier.
+Instantiation of the generic simplifier for HOL.
*)
section "Simplifier";
@@ -56,6 +56,7 @@
fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
end;
+
qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
(fn [prem] => [rewtac prem, rtac refl 1]);
@@ -69,32 +70,19 @@
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
- fun atomize pairs =
- let fun atoms th =
- (case concl_of th of
- Const("Trueprop",_) $ p =>
- (case head_of p of
- Const(a,_) =>
- (case assoc(pairs,a) of
- Some(rls) => flat (map atoms ([th] RL rls))
- | None => [th])
- | _ => [th])
- | _ => [th])
- in atoms end;
-
- fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
in
- fun mk_meta_eq r = r RS eq_reflection;
+ fun meta_eq r = r RS eq_reflection;
+
+ fun mk_meta_eq th = case concl_of th of
+ Const("==",_)$_$_ => th
+ | _$(Const("op =",_)$_$_) => meta_eq th
+ | _$(Const("Not",_)$_) => th RS not_P_imp_P_eq_False
+ | _ => th RS P_imp_P_eq_True;
+ (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+
fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
- fun mk_meta_eq_simp r = case concl_of r of
- Const("==",_)$_$_ => r
- | _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
- | _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
- | _ => r RS P_imp_P_eq_True;
- (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
val simp_thms = map prover
[ "(x=x) = True",
@@ -122,7 +110,7 @@
infix 4 addcongs delcongs;
fun mk_meta_cong rl =
- standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+ standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must be =-equalities");
@@ -133,8 +121,6 @@
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
-fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
-
val imp_cong = impI RSN
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [Blast_tac 1]) RS mp RS mp);
@@ -249,9 +235,6 @@
prove "eq_sym_conv" "(x=y) = (y=x)";
-qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
- (K [rtac refl 1]);
-
(** if-then-else rules **)
@@ -261,12 +244,9 @@
qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
(K [Blast_tac 1]);
-qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
- (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
-(*
-qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y"
- (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
-*)
+qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
+ (K [Blast_tac 1]);
+
qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
(K [Blast_tac 1]);
@@ -284,6 +264,12 @@
(K [stac split_if 1,
Blast_tac 1]);
+qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
+ (K [stac split_if 1, Blast_tac 1]);
+
+qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
+ (K [stac split_if 1, Blast_tac 1]);
+
(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
qed_goal "if_bool_eq_conj" HOL.thy
"(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -339,42 +325,29 @@
(*** Case splitting ***)
-local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_inside_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-val split_asm_tac = mk_case_split_asm_tac split_tac
- (disjE,conjE,exE,contrapos,contrapos2,notnotD);
-
-infix 4 addsplits delsplits;
+structure SplitterData =
+ struct
+ structure Simplifier = Simplifier
+ val mk_meta_eq = mk_meta_eq
+ val meta_eq_to_iff = meta_eq_to_obj_eq
+ val iffD = iffD2
+ val disjE = disjE
+ val conjE = conjE
+ val exE = exE
+ val contrapos = contrapos
+ val contrapos2 = contrapos2
+ val notnotD = notnotD
+ end;
-fun ss addsplits splits =
- let fun addsplit (ss,split) =
- let val (name,asm) = split_thm_info split
- in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
- (if asm then split_asm_tac else split_tac) [split]) end
- in foldl addsplit (ss,splits) end;
+structure Splitter = SplitterFun(SplitterData);
-fun ss delsplits splits =
- let fun delsplit(ss,split) =
- let val (name,asm) = split_thm_info split
- in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
- in foldl delsplit (ss,splits) end;
-
-fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
-fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
-
-qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
- (K [split_tac [split_if] 1, Blast_tac 1]);
-
-qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
- (K [split_tac [split_if] 1, Blast_tac 1]);
+val split_tac = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac = Splitter.split_asm_tac;
+val addsplits = Splitter.addsplits;
+val delsplits = Splitter.delsplits;
+val Addsplits = Splitter.Addsplits;
+val Delsplits = Splitter.Delsplits;
(** 'if' congruence rules: neither included by default! *)
@@ -402,11 +375,32 @@
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
grounds that it allows simplification of R in the two cases.*)
+fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
+
val mksimps_pairs =
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
("All", [spec]), ("True", []), ("False", []),
("If", [if_bool_eq_conj RS iffD1])];
+(* FIXME: move to Provers/simplifier.ML
+val mk_atomize: (string * thm list) list -> thm -> thm list
+*)
+(* FIXME: move to Provers/simplifier.ML*)
+fun mk_atomize pairs =
+ let fun atoms th =
+ (case concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case head_of p of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
+
+fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
+
fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
atac, etac FalseE];
(*No premature instantiation of variables during simplification*)
@@ -424,9 +418,9 @@
([triv_forall_equality, (* prunes params *)
True_implies_equals, (* prune asms `True' *)
if_True, if_False, if_cancel, if_eq_cancel,
- o_apply, imp_disjL, conj_assoc, disj_assoc,
+ imp_disjL, conj_assoc, disj_assoc,
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
- disj_not1, not_all, not_ex, cases_simp]
+ disj_not1, not_all, not_ex, cases_simp, Eps_eq]
@ ex_simps @ all_simps @ simp_thms)
addsimprocs [defALL_regroup,defEX_regroup]
addcongs [imp_cong]
@@ -436,9 +430,6 @@
"f(if c then x else y) = (if c then f x else f y)"
(K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
-qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
- (K [rtac ext 1, rtac refl 1]);
-
(*For expand_case_tac*)
val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
@@ -462,19 +453,6 @@
(*** integration of simplifier with classical reasoner ***)
-(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
- fails if there is no equaliy or if an equality is already at the front *)
-local
- fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
- | is_eq _ = false;
- val find_eq = find_index is_eq;
-in
-val rot_eq_tac =
- SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
- if n>0 then rotate_tac n i else no_tac end)
-end;
-
-
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
val op addcongs = op addcongs and op delcongs = op delcongs