src/FOLP/simpdata.ML
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 17480 fd19f77dcf60
child 26322 eaf634e975fa
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1463
49ca5e875691 expanded tabs
clasohm
parents: 1459
diff changeset
     1
(*  Title:      FOLP/simpdata.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
     6
Simplification data for FOLP.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*** Rewrite rules ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
    11
fun int_prove_fun_raw s =
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
    12
    (writeln s;  prove_goal (the_context ()) s
2603
4988dda71c0b Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents: 1463
diff changeset
    13
       (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val conj_rews = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    18
 ["P & True <-> P",     "True & P <-> P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  "P & False <-> False", "False & P <-> False",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  "P & P <-> P",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    21
  "P & ~P <-> False",   "~P & P <-> False",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  "(P & Q) & R <-> P & (Q & R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val disj_rews = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    25
 ["P | True <-> True",  "True | P <-> True",
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    26
  "P | False <-> P",    "False | P <-> P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  "P | P <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  "(P | Q) | R <-> P | (Q | R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val not_rews = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    31
 ["~ False <-> True",   "~ True <-> False"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val imp_rews = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    34
 ["(P --> False) <-> ~P",       "(P --> True) <-> True",
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
    35
  "(False --> P) <-> True",     "(True --> P) <-> P",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    36
  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val iff_rews = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    39
 ["(True <-> P) <-> P",         "(P <-> True) <-> P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  "(P <-> P) <-> True",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    41
  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val quant_rews = map int_prove_fun
3836
f1a1817659e6 fixed dots;
wenzelm
parents: 2603
diff changeset
    44
 ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
(*These are NOT supplied by default!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val distrib_rews  = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
 ["~(P|Q) <-> ~P & ~Q",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  "(P | Q --> R) <-> (P --> R) & (Q --> R)",
3836
f1a1817659e6 fixed dots;
wenzelm
parents: 2603
diff changeset
    51
  "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
f1a1817659e6 fixed dots;
wenzelm
parents: 2603
diff changeset
    52
  "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
f1a1817659e6 fixed dots;
wenzelm
parents: 2603
diff changeset
    53
  "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
f1a1817659e6 fixed dots;
wenzelm
parents: 2603
diff changeset
    54
  "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun make_iff_T th = th RS P_Imp_P_iff_T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val refl_iff_T = make_iff_T refl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val norm_thms = [(norm_eq RS sym, norm_eq),
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
    63
                 (NORM_iff RS iff_sym, NORM_iff)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(* Conversion into rewrite rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
fun mk_eq th = case concl_of th of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
      _ $ (Const("op <->",_)$_$_) $ _ => th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    | _ $ (Const("op =",_)$_$_) $ _ => th
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
    73
    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    | _ => make_iff_T th;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    76
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    77
val mksimps_pairs =
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    78
  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    79
   ("All", [spec]), ("True", []), ("False", [])];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    81
fun mk_atomize pairs =
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    82
  let fun atoms th =
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    83
        (case concl_of th of
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    84
           Const("Trueprop",_) $ p =>
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    85
             (case head_of p of
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    86
                Const(a,_) =>
17325
d9d50222808e introduced new-style AList operations
haftmann
parents: 15570
diff changeset
    87
                  (case AList.lookup (op =) pairs a of
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    88
                     SOME(rls) => List.concat (map atoms ([th] RL rls))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 5304
diff changeset
    89
                   | NONE => [th])
5304
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    90
              | _ => [th])
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    91
         | _ => [th])
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    92
  in atoms end;
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    93
c133f16febc7 the splitter is now defined as a functor
oheimb
parents: 3836
diff changeset
    94
fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
(*destruct function for analysing equations*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  | dest_red t = raise TERM("FOL/dest_red", [t]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
structure FOLP_SimpData : SIMP_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  struct
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   102
  val refl_thms         = [refl, iff_refl]
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   103
  val trans_thms        = [trans, iff_trans]
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   104
  val red1              = iffD1
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   105
  val red2              = iffD2
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   106
  val mk_rew_rules      = mk_rew_rules
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   107
  val case_splits       = []         (*NO IF'S!*)
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   108
  val norm_thms         = norm_thms
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   109
  val subst_thms        = [subst];
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   110
  val dest_red          = dest_red
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
structure FOLP_Simp = SimpFun(FOLP_SimpData);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
   116
val FOLP_congs =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
   [all_cong,ex_cong,eq_cong,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
    conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
val IFOLP_rews =
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
   121
   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    imp_rews @ iff_rews @ quant_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
1009
eb7c50688405 No longer builds the induction structure (from ../Provers/ind.ML)
lcp
parents: 0
diff changeset
   124
open FOLP_Simp;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val auto_ss = empty_ss setauto ares_tac [TrueI];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
(*Classical version...*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
   131
fun prove_fun s =
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 17325
diff changeset
   132
    (writeln s;  prove_goal (the_context ()) s
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val cla_rews = map prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   136
 ["?p:P | ~P",          "?p:~P | P",
d12da312eff4 expanded tabs
clasohm
parents: 1009
diff changeset
   137
  "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val FOLP_rews = IFOLP_rews@cla_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;