src/FOLP/simpdata.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1463 49ca5e875691
child 2603 4988dda71c0b
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@1463
     1
(*  Title:      FOLP/simpdata.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@1463
     6
Simplification data for FOLP
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*** Rewrite rules ***)
clasohm@0
    10
clasohm@0
    11
fun int_prove_fun_raw s = 
clasohm@0
    12
    (writeln s;  prove_goal IFOLP.thy s
clasohm@0
    13
       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
clasohm@0
    14
clasohm@0
    15
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
clasohm@0
    16
clasohm@0
    17
val conj_rews = map int_prove_fun
clasohm@1459
    18
 ["P & True <-> P",     "True & P <-> P",
clasohm@0
    19
  "P & False <-> False", "False & P <-> False",
clasohm@0
    20
  "P & P <-> P",
clasohm@1459
    21
  "P & ~P <-> False",   "~P & P <-> False",
clasohm@0
    22
  "(P & Q) & R <-> P & (Q & R)"];
clasohm@0
    23
clasohm@0
    24
val disj_rews = map int_prove_fun
clasohm@1459
    25
 ["P | True <-> True",  "True | P <-> True",
clasohm@1459
    26
  "P | False <-> P",    "False | P <-> P",
clasohm@0
    27
  "P | P <-> P",
clasohm@0
    28
  "(P | Q) | R <-> P | (Q | R)"];
clasohm@0
    29
clasohm@0
    30
val not_rews = map int_prove_fun
clasohm@1459
    31
 ["~ False <-> True",   "~ True <-> False"];
clasohm@0
    32
clasohm@0
    33
val imp_rews = map int_prove_fun
clasohm@1459
    34
 ["(P --> False) <-> ~P",       "(P --> True) <-> True",
clasohm@1459
    35
  "(False --> P) <-> True",     "(True --> P) <-> P", 
clasohm@1459
    36
  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
clasohm@0
    37
clasohm@0
    38
val iff_rews = map int_prove_fun
clasohm@1459
    39
 ["(True <-> P) <-> P",         "(P <-> True) <-> P",
clasohm@0
    40
  "(P <-> P) <-> True",
clasohm@1459
    41
  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
clasohm@0
    42
clasohm@0
    43
val quant_rews = map int_prove_fun
clasohm@1459
    44
 ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
clasohm@0
    45
clasohm@0
    46
(*These are NOT supplied by default!*)
clasohm@0
    47
val distrib_rews  = map int_prove_fun
clasohm@0
    48
 ["~(P|Q) <-> ~P & ~Q",
clasohm@0
    49
  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
clasohm@0
    50
  "(P | Q --> R) <-> (P --> R) & (Q --> R)",
clasohm@0
    51
  "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
clasohm@0
    52
  "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
clasohm@0
    53
  "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
clasohm@0
    54
  "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
clasohm@0
    55
clasohm@0
    56
val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
clasohm@0
    57
clasohm@0
    58
fun make_iff_T th = th RS P_Imp_P_iff_T;
clasohm@0
    59
clasohm@0
    60
val refl_iff_T = make_iff_T refl;
clasohm@0
    61
clasohm@0
    62
val norm_thms = [(norm_eq RS sym, norm_eq),
clasohm@1459
    63
                 (NORM_iff RS iff_sym, NORM_iff)];
clasohm@0
    64
clasohm@0
    65
clasohm@0
    66
(* Conversion into rewrite rules *)
clasohm@0
    67
clasohm@0
    68
val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
clasohm@0
    69
clasohm@0
    70
fun mk_eq th = case concl_of th of
clasohm@0
    71
      _ $ (Const("op <->",_)$_$_) $ _ => th
clasohm@0
    72
    | _ $ (Const("op =",_)$_$_) $ _ => th
clasohm@0
    73
    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
clasohm@0
    74
    | _ => make_iff_T th;
clasohm@0
    75
clasohm@0
    76
fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
clasohm@0
    77
      _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
clasohm@0
    78
    | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
clasohm@1459
    79
                                       atomize(th RS conjunct2)
clasohm@0
    80
    | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
clasohm@0
    81
    | _ $ (Const("True",_)) $ _ => []
clasohm@0
    82
    | _ $ (Const("False",_)) $ _ => []
clasohm@0
    83
    | _ => [th];
clasohm@0
    84
clasohm@0
    85
fun mk_rew_rules th = map mk_eq (atomize th);
clasohm@0
    86
clasohm@0
    87
(*destruct function for analysing equations*)
clasohm@0
    88
fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
clasohm@0
    89
  | dest_red t = raise TERM("FOL/dest_red", [t]);
clasohm@0
    90
clasohm@0
    91
structure FOLP_SimpData : SIMP_DATA =
clasohm@0
    92
  struct
clasohm@1459
    93
  val refl_thms         = [refl, iff_refl]
clasohm@1459
    94
  val trans_thms        = [trans, iff_trans]
clasohm@1459
    95
  val red1              = iffD1
clasohm@1459
    96
  val red2              = iffD2
clasohm@1459
    97
  val mk_rew_rules      = mk_rew_rules
clasohm@1459
    98
  val case_splits       = []         (*NO IF'S!*)
clasohm@1459
    99
  val norm_thms         = norm_thms
clasohm@1459
   100
  val subst_thms        = [subst];
clasohm@1459
   101
  val dest_red          = dest_red
clasohm@0
   102
  end;
clasohm@0
   103
clasohm@0
   104
structure FOLP_Simp = SimpFun(FOLP_SimpData);
clasohm@0
   105
clasohm@0
   106
(*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
clasohm@0
   107
val FOLP_congs = 
clasohm@0
   108
   [all_cong,ex_cong,eq_cong,
clasohm@0
   109
    conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
clasohm@0
   110
clasohm@0
   111
val IFOLP_rews =
clasohm@0
   112
   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
clasohm@0
   113
    imp_rews @ iff_rews @ quant_rews;
clasohm@0
   114
lcp@1009
   115
open FOLP_Simp;
clasohm@0
   116
clasohm@0
   117
val auto_ss = empty_ss setauto ares_tac [TrueI];
clasohm@0
   118
clasohm@0
   119
val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
clasohm@0
   120
clasohm@0
   121
(*Classical version...*)
clasohm@0
   122
fun prove_fun s = 
clasohm@0
   123
    (writeln s;  prove_goal FOLP.thy s
clasohm@0
   124
       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
clasohm@0
   125
clasohm@0
   126
val cla_rews = map prove_fun
clasohm@1459
   127
 ["?p:P | ~P",          "?p:~P | P",
clasohm@1459
   128
  "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
clasohm@0
   129
clasohm@0
   130
val FOLP_rews = IFOLP_rews@cla_rews;
clasohm@0
   131
clasohm@0
   132
val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
clasohm@0
   133
clasohm@0
   134