author | wenzelm |
Sun, 02 Sep 2018 22:54:51 +0200 | |
changeset 68886 | 1167f2d8a167 |
parent 61268 | abe08fb15a12 |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
1 |
(* Title: Sequents/simpdata.ML |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
3 |
Copyright 1999 University of Cambridge |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
4 |
|
27149 | 5 |
Instantiation of the generic simplifier for LK. |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
6 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
7 |
Borrows from the DC simplifier of Soren Heilmann. |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
8 |
*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
9 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
10 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
11 |
(** Conversion into rewrite rules **) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
12 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
13 |
(*Make atomic rewrite rules*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
14 |
fun atomize r = |
59582 | 15 |
case Thm.concl_of r of |
38500 | 16 |
Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
55228 | 17 |
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of |
9713 | 18 |
([], [p]) => |
19 |
(case p of |
|
38500 | 20 |
Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R}) |
21 |
| Const(@{const_name conj},_)$_$_ => atomize(r RS @{thm conjunct1}) @ |
|
22896 | 22 |
atomize(r RS @{thm conjunct2}) |
38500 | 23 |
| Const(@{const_name All},_)$_ => atomize(r RS @{thm spec}) |
24 |
| Const(@{const_name True},_) => [] (*True is DELETED*) |
|
25 |
| Const(@{const_name False},_) => [] (*should False do something?*) |
|
9713 | 26 |
| _ => [r]) |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
27 |
| _ => []) (*ignore theorem unless it has precisely one conclusion*) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
28 |
| _ => [r]; |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
29 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
30 |
(*Make meta-equalities.*) |
59582 | 31 |
fun mk_meta_eq ctxt th = case Thm.concl_of th of |
56245 | 32 |
Const(@{const_name Pure.eq},_)$_$_ => th |
38500 | 33 |
| Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
55228 | 34 |
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of |
9713 | 35 |
([], [p]) => |
36 |
(case p of |
|
38500 | 37 |
(Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection} |
38 |
| (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} |
|
39 |
| (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} |
|
27149 | 40 |
| _ => th RS @{thm iff_reflection_T}) |
61268 | 41 |
| _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
42 |
|
7123 | 43 |
(*Replace premises x=y, X<->Y by X==Y*) |
36546 | 44 |
fun mk_meta_prems ctxt = |
45 |
rule_by_tactic ctxt |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
46 |
(REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
7123 | 47 |
|
9713 | 48 |
(*Congruence rules for = or <-> (instead of ==)*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
49 |
fun mk_meta_cong ctxt rl = |
55228 | 50 |
Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl)) |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset
|
51 |
handle THM _ => |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset
|
52 |
error("Premises and conclusion of congruence rules must use =-equality or <->"); |
7123 | 53 |
|
54 |
||
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
55 |
(*** Standard simpsets ***) |
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
56 |
|
27149 | 57 |
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, |
58 |
@{thm iff_refl}, reflexive_thm]; |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
59 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
60 |
fun unsafe_solver ctxt = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
61 |
FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt]; |
27149 | 62 |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
63 |
(*No premature instantiation of variables during simplification*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
64 |
fun safe_solver ctxt = |
58957 | 65 |
FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i), |
66 |
eq_assume_tac]; |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
67 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
68 |
(*No simprules, but basic infrastructure for simplification*) |
9713 | 69 |
val LK_basic_ss = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
70 |
empty_simpset @{context} |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
71 |
setSSolver (mk_solver "safe" safe_solver) |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
72 |
setSolver (mk_solver "unsafe" unsafe_solver) |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
73 |
|> Simplifier.set_subgoaler asm_simp_tac |
60822 | 74 |
|> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
75 |
|> Simplifier.set_mkcong mk_meta_cong |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
76 |
|> simpset_of; |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
77 |
|
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
78 |
val LK_simps = |
46186 | 79 |
[@{thm triv_forall_equality}, (* prunes params *) |
27149 | 80 |
@{thm refl} RS @{thm P_iff_T}] @ |
81 |
@{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ |
|
82 |
@{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @ |
|
83 |
@{thms all_simps} @ @{thms ex_simps} @ |
|
84 |
[@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ |
|
85 |
@{thms LK_extra_simps}; |
|
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
86 |
|
9713 | 87 |
val LK_ss = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
88 |
put_simpset LK_basic_ss @{context} addsimps LK_simps |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
43597
diff
changeset
|
89 |
|> Simplifier.add_eqcong @{thm left_cong} |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
90 |
|> Simplifier.add_cong @{thm imp_cong} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset
|
91 |
|> simpset_of; |
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset
|
92 |