src/Sequents/simpdata.ML
author wenzelm
Thu, 23 Jul 2009 23:12:21 +0200
changeset 32155 e2bf2f73b0c8
parent 32091 30e2ffbba718
child 32957 675c0c7e6a37
permissions -rw-r--r--
more @{theory} antiquotations;
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
    ID:         $Id$
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
     5
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
     6
Instantiation of the generic simplifier for LK.
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
     7
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
     8
Borrows from the DC simplifier of Soren Heilmann.
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
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    12
(** Conversion into rewrite rules **)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    13
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    14
(*Make atomic rewrite rules*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    15
fun atomize r =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    16
 case concl_of r of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    17
   Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    18
     (case (forms_of_seq a, forms_of_seq c) of
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    19
        ([], [p]) =>
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    20
          (case p of
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    21
               Const("imp",_)$_$_ => atomize(r RS @{thm mp_R})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    22
             | Const("conj",_)$_$_   => atomize(r RS @{thm conjunct1}) @
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    23
                   atomize(r RS @{thm conjunct2})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    24
             | Const("All",_)$_      => atomize(r RS @{thm spec})
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    25
             | Const("True",_)       => []    (*True is DELETED*)
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    26
             | Const("False",_)      => []    (*should False do something?*)
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    27
             | _                     => [r])
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    28
      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    29
 | _ => [r];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    30
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    31
(*Make meta-equalities.*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    32
fun mk_meta_eq th = case concl_of th of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    33
    Const("==",_)$_$_           => th
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    34
  | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    35
        (case (forms_of_seq a, forms_of_seq c) of
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    36
             ([], [p]) =>
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    37
                 (case p of
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    38
                      (Const("equal",_)$_$_)   => th RS @{thm eq_reflection}
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    39
                    | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    40
                    | (Const("Not",_)$_)      => th RS @{thm iff_reflection_F}
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    41
                    | _                       => th RS @{thm iff_reflection_T})
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    42
           | _ => 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
    43
                         Display.string_of_thm_without_context th));
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    44
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    45
(*Replace premises x=y, X<->Y by X==Y*)
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    46
val mk_meta_prems =
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    47
    rule_by_tactic
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21428
diff changeset
    48
      (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
    49
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    50
(*Congruence rules for = or <-> (instead of ==)*)
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    51
fun mk_meta_cong rl =
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    52
  standard(mk_meta_eq (mk_meta_prems rl))
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    53
  handle THM _ =>
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    54
  error("Premises and conclusion of congruence rules must use =-equality or <->");
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    55
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    56
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    57
(*** Standard simpsets ***)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    58
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    59
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    60
  @{thm iff_refl}, reflexive_thm];
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    61
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    62
fun unsafe_solver prems =
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    63
  FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    64
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    65
(*No premature instantiation of variables during simplification*)
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    66
fun safe_solver prems =
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    67
 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
    68
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    69
(*No simprules, but basic infrastructure for simplification*)
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    70
val LK_basic_ss =
32155
e2bf2f73b0c8 more @{theory} antiquotations;
wenzelm
parents: 32091
diff changeset
    71
  Simplifier.theory_context @{theory} empty_ss
17892
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17876
diff changeset
    72
    setsubgoaler asm_simp_tac
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    73
    setSSolver (mk_solver "safe" safe_solver)
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    74
    setSolver (mk_solver "unsafe" unsafe_solver)
12725
7ede865e1fe5 renamed forall_elim_vars_safe to gen_all;
wenzelm
parents: 12720
diff changeset
    75
    setmksimps (map mk_meta_eq o atomize o gen_all)
9713
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    76
    setmkcong mk_meta_cong;
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 =
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7098
diff changeset
    79
   [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 =
2c5b42311eb0 cong setup now part of Simplifier;
wenzelm
parents: 9259
diff changeset
    88
  LK_basic_ss addsimps LK_simps
27149
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    89
  addeqcongs [@{thm left_cong}]
123377499a8e converted ML proofs from simpdata.ML;
wenzelm
parents: 26928
diff changeset
    90
  addcongs [@{thm imp_cong}];
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    91
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17481
diff changeset
    92
change_simpset (fn _ => LK_ss);