src/Sequents/simpdata.ML
author haftmann
Thu, 18 Nov 2010 17:01:15 +0100
changeset 40602 91e583511113
parent 38500 d5477ee35820
child 42795 66fcc9882784
permissions -rw-r--r--
map_fun combinator in theory Fun
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 =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    15
 case concl_of r of
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    16
   Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    17
     (case (forms_of_seq a, 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.*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    31
fun mk_meta_eq th = case concl_of th of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    32
    Const("==",_)$_$_           => th
38500
d5477ee35820 more antiquotations
haftmann
parents: 36546
diff changeset
    33
  | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    34
        (case (forms_of_seq a, forms_of_seq c) of
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})
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    41
           | _ => error ("addsimps: unable to use theorem\n" ^
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 27149
diff changeset
    42
                         Display.string_of_thm_without_context th));
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    43
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    44
(*Replace premises x=y, X<->Y by X==Y*)
36546
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    45
fun mk_meta_prems ctxt =
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    46
    rule_by_tactic ctxt
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    47
      (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    48
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    49
(*Congruence rules for = or <-> (instead of ==)*)
36546
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    50
fun mk_meta_cong ss rl =
a9873318fe30 proper context for rule_by_tactic;
wenzelm
parents: 36543
diff changeset
    51
  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) 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
    52
    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
    53
      error("Premises and conclusion of congruence rules must use =-equality or <->");
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    54
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    55
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    56
(*** Standard simpsets ***)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    57
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    58
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    59
  @{thm iff_refl}, reflexive_thm];
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    60
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    61
fun unsafe_solver prems =
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    62
  FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    63
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    64
(*No premature instantiation of variables during simplification*)
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    65
fun safe_solver prems =
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    66
 FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), 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 =
35232
f588e1169c8b renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents: 35021
diff changeset
    70
  Simplifier.global_context @{theory} empty_ss
17892
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17876
diff changeset
    71
    setsubgoaler asm_simp_tac
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    72
    setSSolver (mk_solver "safe" safe_solver)
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    73
    setSolver (mk_solver "unsafe" unsafe_solver)
36543
0e7fc5bf38de proper context for mksimps etc. -- via simpset of the running Simplifier;
wenzelm
parents: 35762
diff changeset
    74
    setmksimps (K (map mk_meta_eq o atomize o gen_all))
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    75
    setmkcong mk_meta_cong;
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    76
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    77
val LK_simps =
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    78
   [triv_forall_equality, (* prunes params *)
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    79
    @{thm refl} RS @{thm P_iff_T}] @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    80
    @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    81
    @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    82
    @{thms all_simps} @ @{thms ex_simps} @
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    83
    [@{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
    84
    @{thms LK_extra_simps};
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    85
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    86
val LK_ss =
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    87
  LK_basic_ss addsimps LK_simps
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    88
  addeqcongs [@{thm left_cong}]
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    89
  addcongs [@{thm imp_cong}];
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    90
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17481
diff changeset
    91
change_simpset (fn _ => LK_ss);