--- a/src/HOL/HOL.thy Fri Nov 03 14:22:36 2006 +0100
+++ b/src/HOL/HOL.thy Fri Nov 03 14:22:37 2006 +0100
@@ -7,7 +7,7 @@
theory HOL
imports CPure
-uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") "Tools/res_atpset.ML"
+uses ("simpdata.ML") "Tools/res_atpset.ML"
begin
subsection {* Primitive logic *}
@@ -861,8 +861,34 @@
lemma thin_refl:
"\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
-use "cladata.ML"
-setup Hypsubst.hypsubst_setup
+ML {*
+structure Hypsubst = HypsubstFun(
+struct
+ structure Simplifier = Simplifier
+ val dest_eq = HOLogic.dest_eq_typ
+ val dest_Trueprop = HOLogic.dest_Trueprop
+ val dest_imp = HOLogic.dest_imp
+ val eq_reflection = HOL.eq_reflection
+ val rev_eq_reflection = HOL.def_imp_eq
+ val imp_intr = HOL.impI
+ val rev_mp = HOL.rev_mp
+ val subst = HOL.subst
+ val sym = HOL.sym
+ val thin_refl = thm "thin_refl";
+end);
+
+structure Classical = ClassicalFun(
+struct
+ val mp = HOL.mp
+ val not_elim = HOL.notE
+ val classical = HOL.classical
+ val sizef = Drule.size_of_thm
+ val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
+end);
+
+structure BasicClassical: BASIC_CLASSICAL = Classical;
+*}
+
setup {*
let
(*prevent substitution on bool*)
@@ -870,11 +896,12 @@
Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
(nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
in
- ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+ Hypsubst.hypsubst_setup
+ #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+ #> Classical.setup
+ #> ResAtpset.setup
end
*}
-setup Classical.setup
-setup ResAtpset.setup
declare iffI [intro!]
and notI [intro!]
@@ -891,17 +918,6 @@
and conjE [elim!]
and conjE [elim!]
-ML {*
-structure HOL =
-struct
-
-open HOL;
-
-val claset_prop = Classical.claset_of (the_context ());
-
-end;
-*}
-
declare ex_ex1I [intro!]
and allI [intro!]
and the_equality [intro]
@@ -943,15 +959,31 @@
apply (tactic "etac (Classical.dup_elim HOL.allE) 1")
by iprover
-use "blastdata.ML"
-setup Blast.setup
+ML {*
+structure Blast = BlastFun(
+struct
+ type claset = Classical.claset
+ val equality_name = "op ="
+ val not_name = "Not"
+ val notE = HOL.notE
+ val ccontr = HOL.ccontr
+ val contr_tac = Classical.contr_tac
+ val dup_intr = Classical.dup_intr
+ val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+ val claset = Classical.claset
+ val rep_cs = Classical.rep_cs
+ val cla_modifiers = Classical.cla_modifiers
+ val cla_meth' = Classical.cla_meth'
+end);
-ML {*
structure HOL =
struct
open HOL;
+val Blast_tac = Blast.Blast_tac;
+val blast_tac = Blast.blast_tac;
+
fun case_tac a = res_inst_tac [("P", a)] case_split;
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
@@ -967,9 +999,6 @@
fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
-val Blast_tac = Blast.Blast_tac;
-val blast_tac = Blast.blast_tac;
-
fun Trueprop_conv conv ct = (case term_of ct of
Const ("Trueprop", _) $ _ =>
let val (ct1, ct2) = Thm.dest_comb ct
@@ -1002,6 +1031,8 @@
end;
*}
+setup Blast.setup
+
subsubsection {* Simplifier *}
@@ -1042,29 +1073,6 @@
"!!P. (ALL x. t=x --> P(x)) = P(t)"
by (blast, blast, blast, blast, blast, iprover+)
-lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
- by iprover
-
-lemma ex_simps:
- "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)"
- "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))"
- "!!P Q. (EX x. P x | Q) = ((EX x. P x) | Q)"
- "!!P Q. (EX x. P | Q x) = (P | (EX x. Q x))"
- "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
- "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
- -- {* Miniscoping: pushing in existential quantifiers. *}
- by (iprover | blast)+
-
-lemma all_simps:
- "!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)"
- "!!P Q. (ALL x. P & Q x) = (P & (ALL x. Q x))"
- "!!P Q. (ALL x. P x | Q) = ((ALL x. P x) | Q)"
- "!!P Q. (ALL x. P | Q x) = (P | (ALL x. Q x))"
- "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
- "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
- -- {* Miniscoping: pushing in universal quantifiers. *}
- by (iprover | blast)+
-
lemma disj_absorb: "(A | A) = A"
by blast
@@ -1114,6 +1122,9 @@
lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
+lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
+ by iprover
+
lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
@@ -1257,18 +1268,6 @@
by (rule equal_elim_rule1)
qed
-
-text {* \medskip Actual Installation of the Simplifier. *}
-
-lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
-proof
- assume prem: "True \<Longrightarrow> PROP P"
- from prem [OF TrueI] show "PROP P" .
-next
- assume "PROP P"
- show "PROP P" .
-qed
-
lemma uncurry:
assumes "P \<longrightarrow> Q \<longrightarrow> R"
shows "P \<and> Q \<longrightarrow> R"
@@ -1293,11 +1292,42 @@
by blast
use "simpdata.ML"
-setup "Simplifier.method_setup Splitter.split_modifiers"
-setup "(fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))"
-setup Splitter.setup
-setup Clasimp.setup
-setup EqSubst.setup
+setup {*
+ Simplifier.method_setup Splitter.split_modifiers
+ #> (fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))
+ #> Splitter.setup
+ #> Clasimp.setup
+ #> EqSubst.setup
+*}
+
+lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+proof
+ assume prem: "True \<Longrightarrow> PROP P"
+ from prem [OF TrueI] show "PROP P" .
+next
+ assume "PROP P"
+ show "PROP P" .
+qed
+
+lemma ex_simps:
+ "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)"
+ "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))"
+ "!!P Q. (EX x. P x | Q) = ((EX x. P x) | Q)"
+ "!!P Q. (EX x. P | Q x) = (P | (EX x. Q x))"
+ "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
+ "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
+ -- {* Miniscoping: pushing in existential quantifiers. *}
+ by (iprover | blast)+
+
+lemma all_simps:
+ "!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)"
+ "!!P Q. (ALL x. P & Q x) = (P & (ALL x. Q x))"
+ "!!P Q. (ALL x. P x | Q) = ((ALL x. P x) | Q)"
+ "!!P Q. (ALL x. P | Q x) = (P | (ALL x. Q x))"
+ "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
+ "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
+ -- {* Miniscoping: pushing in universal quantifiers. *}
+ by (iprover | blast)+
declare triv_forall_equality [simp] (*prunes params*)
and True_implies_equals [simp] (*prune asms `True'*)
--- a/src/HOL/IsaMakefile Fri Nov 03 14:22:36 2006 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 03 14:22:37 2006 +0100
@@ -119,7 +119,7 @@
Tools/typedef_package.ML Tools/typedef_codegen.ML \
Transitive_Closure.ML Transitive_Closure.thy \
Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \
- arith_data.ML blastdata.ML cladata.ML \
+ arith_data.ML \
document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy \
Tools/res_atp_provers.ML Tools/res_atp_methods.ML \
Tools/res_hol_clause.ML \
--- a/src/HOL/cladata.ML Fri Nov 03 14:22:36 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: HOL/cladata.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1996 University of Cambridge
-
-Setting up the classical reasoner.
-*)
-
-structure Hypsubst_Data =
-struct
- structure Simplifier = Simplifier
- val dest_eq = HOLogic.dest_eq_typ
- val dest_Trueprop = HOLogic.dest_Trueprop
- val dest_imp = HOLogic.dest_imp
- val eq_reflection = HOL.eq_reflection
- val rev_eq_reflection = HOL.def_imp_eq
- val imp_intr = HOL.impI
- val rev_mp = HOL.rev_mp
- val subst = HOL.subst
- val sym = HOL.sym
- val thin_refl = thm "thin_refl";
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-
-structure Classical_Data =
-struct
- val mp = HOL.mp
- val not_elim = HOL.notE
- val classical = HOL.classical
- val sizef = Drule.size_of_thm
- val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
-end;
-
-structure Classical = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Classical;
--- a/src/HOL/simpdata.ML Fri Nov 03 14:22:36 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,318 +0,0 @@
-(* Title: HOL/simpdata.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1991 University of Cambridge
-
-Instantiation of the generic simplifier for HOL.
-*)
-
-(** tools setup **)
-
-structure Quantifier1 = Quantifier1Fun
-(struct
- (*abstract syntax*)
- fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
- | dest_eq _ = NONE;
- fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
- | dest_conj _ = NONE;
- fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
- | dest_imp _ = NONE;
- val conj = HOLogic.conj
- val imp = HOLogic.imp
- (*rules*)
- val iff_reflection = HOL.eq_reflection
- val iffI = HOL.iffI
- val iff_trans = HOL.trans
- val conjI= HOL.conjI
- val conjE= HOL.conjE
- val impI = HOL.impI
- val mp = HOL.mp
- val uncurry = thm "uncurry"
- val exI = HOL.exI
- val exE = HOL.exE
- 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);
-
-structure HOL =
-struct
-
-open HOL;
-
-val Eq_FalseI = thm "Eq_FalseI";
-val Eq_TrueI = thm "Eq_TrueI";
-val simp_implies_def = thm "simp_implies_def";
-val simp_impliesI = thm "simp_impliesI";
-
-fun mk_meta_eq r = r RS eq_reflection;
-fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
-
-fun mk_eq thm = case concl_of thm
- (*expects Trueprop if not == *)
- of Const ("==",_) $ _ $ _ => thm
- | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm
- | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI
- | _ => thm RS Eq_TrueI;
-
-fun mk_eq_True r =
- SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
-
-(* Produce theorems of the form
- (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
-*)
-fun lift_meta_eq_to_obj_eq i st =
- let
- fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
- | count_imp _ = 0;
- val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
- in if j = 0 then meta_eq_to_obj_eq
- else
- let
- val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
- fun mk_simp_implies Q = foldr (fn (R, S) =>
- Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
- val aT = TFree ("'a", HOLogic.typeS);
- val x = Free ("x", aT);
- val y = Free ("y", aT)
- in Goal.prove_global (Thm.theory_of_thm st) []
- [mk_simp_implies (Logic.mk_equals (x, y))]
- (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
- (fn prems => EVERY
- [rewrite_goals_tac [simp_implies_def],
- REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
- end
- end;
-
-(*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl = zero_var_indexes
- (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
- rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
- in mk_meta_eq rl' handle THM _ =>
- if can Logic.dest_equals (concl_of rl') then rl'
- else error "Conclusion of congruence rules must be =-equality"
- end);
-
-(*
-val mk_atomize: (string * thm list) list -> thm -> thm list
-looks too specific to move it somewhere else
-*)
-fun mk_atomize pairs =
- let
- fun atoms thm = case concl_of thm
- of Const("Trueprop", _) $ p => (case head_of p
- of Const(a, _) => (case AList.lookup (op =) pairs a
- of SOME rls => maps atoms ([thm] RL rls)
- | NONE => [thm])
- | _ => [thm])
- | _ => [thm]
- in atoms end;
-
-fun mksimps pairs =
- (map_filter (try mk_eq) o mk_atomize pairs o gen_all);
-
-fun unsafe_solver_tac prems =
- (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
- FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE];
-val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
-
-(*No premature instantiation of variables during simplification*)
-fun safe_solver_tac prems =
- (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
- FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems),
- eq_assume_tac, ematch_tac [FalseE]];
-val safe_solver = mk_solver "HOL safe" safe_solver_tac;
-
-end;
-
-structure SplitterData =
-struct
- structure Simplifier = Simplifier
- val mk_eq = HOL.mk_eq
- val meta_eq_to_iff = HOL.meta_eq_to_obj_eq
- val iffD = HOL.iffD2
- val disjE = HOL.disjE
- val conjE = HOL.conjE
- val exE = HOL.exE
- val contrapos = HOL.contrapos_nn
- val contrapos2 = HOL.contrapos_pp
- val notnotD = HOL.notnotD
-end;
-
-structure Splitter = SplitterFun(SplitterData);
-
-(* integration of simplifier with classical reasoner *)
-
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Splitter = Splitter
- and Classical = Classical and Blast = Blast
- val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
-
-structure HOL =
-struct
-
-open HOL;
-
-val mksimps_pairs =
- [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
- ("All", [spec]), ("True", []), ("False", []),
- ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])];
-
-val simpset_basic =
- Simplifier.theory_context (the_context ()) empty_ss
- setsubgoaler asm_simp_tac
- setSSolver safe_solver
- setSolver unsafe_solver
- setmksimps (mksimps mksimps_pairs)
- setmkeqTrue mk_eq_True
- setmkcong mk_meta_cong;
-
-fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
-
-fun unfold_tac ths =
- let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
- in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
-
-(** simprocs **)
-
-(* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
-
-val use_neq_simproc = ref true;
-
-local
- val thy = the_context ();
- val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI;
- fun neq_prover sg ss (eq $ lhs $ rhs) =
- let
- fun test thm = (case #prop (rep_thm thm) of
- _ $ (Not $ (eq' $ l' $ r')) =>
- Not = HOLogic.Not andalso eq' = eq andalso
- r' aconv lhs andalso l' aconv rhs
- | _ => false)
- in if !use_neq_simproc then case find_first test (prems_of_ss ss)
- of NONE => NONE
- | SOME thm => SOME (thm RS neq_to_EQ_False)
- else NONE
- end
-in
-
-val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
-
-end; (*local*)
-
-
-(* simproc for Let *)
-
-val use_let_simproc = ref true;
-
-local
- val thy = the_context ();
- val Let_folded = thm "Let_folded";
- val Let_unfold = thm "Let_unfold";
- val (f_Let_unfold, x_Let_unfold) =
- let val [(_$(f$x)$_)] = prems_of Let_unfold
- in (cterm_of thy f, cterm_of thy x) end
- val (f_Let_folded, x_Let_folded) =
- let val [(_$(f$x)$_)] = prems_of Let_folded
- in (cterm_of thy f, cterm_of thy x) end;
- val g_Let_folded =
- let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end;
-in
-
-val let_simproc =
- Simplifier.simproc thy "let_simp" ["Let x f"]
- (fn sg => fn ss => fn t =>
- let val ctxt = Simplifier.the_context ss;
- val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
- in Option.map (hd o Variable.export ctxt' ctxt o single)
- (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
- if not (!use_let_simproc) then NONE
- else if is_Free x orelse is_Bound x orelse is_Const x
- then SOME (thm "Let_def")
- else
- let
- val n = case f of (Abs (x,_,_)) => x | _ => "x";
- val cx = cterm_of sg x;
- val {T=xT,...} = rep_cterm cx;
- val cf = cterm_of sg f;
- val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
- val (_$_$g) = prop_of fx_g;
- val g' = abstract_over (x,g);
- in (if (g aconv g')
- then
- let
- val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
- in SOME (rl OF [fx_g]) end
- else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
- else let
- val abs_g'= Abs (n,xT,g');
- val g'x = abs_g'$x;
- val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
- val rl = cterm_instantiate
- [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
- (g_Let_folded,cterm_of sg abs_g')]
- Let_folded;
- in SOME (rl OF [transitive fx_g g_g'x])
- end)
- end
- | _ => NONE)
- end)
-
-end; (*local*)
-
-(* generic refutation procedure *)
-
-(* parameters:
-
- test: term -> bool
- tests if a term is at all relevant to the refutation proof;
- if not, then it can be discarded. Can improve performance,
- esp. if disjunctions can be discarded (no case distinction needed!).
-
- prep_tac: int -> tactic
- A preparation tactic to be applied to the goal once all relevant premises
- have been moved to the conclusion.
-
- ref_tac: int -> tactic
- the actual refutation tactic. Should be able to deal with goals
- [| A1; ...; An |] ==> False
- where the Ai are atomic, i.e. no top-level &, | or EX
-*)
-
-local
- val nnf_simpset =
- empty_ss setmkeqTrue mk_eq_True
- setmksimps (mksimps mksimps_pairs)
- addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj",
- thm "not_all", thm "not_ex", thm "not_not"];
- fun prem_nnf_tac i st =
- full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
-in
-fun refute_tac test prep_tac ref_tac =
- let val refute_prems_tac =
- REPEAT_DETERM
- (eresolve_tac [conjE, exE] 1 ORELSE
- filter_prems_tac test 1 ORELSE
- etac disjE 1) THEN
- ((etac notE 1 THEN eq_assume_tac 1) ORELSE
- ref_tac 1);
- in EVERY'[TRY o filter_prems_tac test,
- REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
- SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
- end;
-end; (*local*)
-
-val defALL_regroup =
- Simplifier.simproc (the_context ())
- "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
-
-val defEX_regroup =
- Simplifier.simproc (the_context ())
- "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
-
-
-val simpset_simprocs = simpset_basic
- addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
-
-end; (*struct*)
\ No newline at end of file