src/Sequents/simpdata.ML
author haftmann
Thu, 23 Nov 2017 17:03:27 +0000
changeset 67087 733017b19de9
parent 61268 abe08fb15a12
child 69593 3dda49e08b9d
permissions -rw-r--r--
generalized more lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
     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
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    15
 case Thm.concl_of r of
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    16
   Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    17
     (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    18
        ([], [p]) =>
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    19
          (case p of
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    20
               Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R})
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    21
             | Const(@{const_name conj},_)$_$_   => atomize(r RS @{thm conjunct1}) @
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    22
                   atomize(r RS @{thm conjunct2})
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    23
             | Const(@{const_name All},_)$_      => atomize(r RS @{thm spec})
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    24
             | Const(@{const_name True},_)       => []    (*True is DELETED*)
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    25
             | Const(@{const_name False},_)      => []    (*should False do something?*)
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    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
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    31
fun mk_meta_eq ctxt th = case Thm.concl_of th of
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55228
diff changeset
    32
    Const(@{const_name Pure.eq},_)$_$_ => th
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    33
  | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    34
        (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    35
             ([], [p]) =>
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    36
                 (case p of
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    37
                      (Const(@{const_name equal},_)$_$_)   => th RS @{thm eq_reflection}
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    38
                    | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    39
                    | (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    40
                    | _                       => th RS @{thm iff_reflection_T})
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60822
diff changeset
    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
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    43
(*Replace premises x=y, X<->Y by X==Y*)
36546
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    44
fun mk_meta_prems ctxt =
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    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
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    47
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    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
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 51717
diff changeset
    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
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    53
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    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
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    57
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    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
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    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
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 56245
diff changeset
    65
  FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 56245
diff changeset
    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
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    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
4f58f3662e7d more explicit context;
wenzelm
parents: 59647
diff changeset
    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
9ae331a1d8c5 more qualified names;
wenzelm
parents: 45659
diff changeset
    79
   [@{thm triv_forall_equality}, (* prunes params *)
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    80
    @{thm refl} RS @{thm P_iff_T}] @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    81
    @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    82
    @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    83
    @{thms all_simps} @ @{thms ex_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    84
    [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    85
    @{thms LK_extra_simps};
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    86
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    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