src/FOL/simpdata.ML
author nipkow
Thu, 16 Sep 1993 16:55:17 +0200
changeset 3 5f77582e3a89
parent 0 a5a9c433f639
child 53 f8f37a9a31dc
permissions -rw-r--r--
defined local addcongs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	FOL/simpdata
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Simplification data for FOL
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
fun int_prove_fun s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    (writeln s;  prove_goal IFOL.thy s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val conj_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
 ["P & True <-> P", 	"True & P <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  "P & False <-> False", "False & P <-> False",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  "P & P <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  "P & ~P <-> False", 	"~P & P <-> False",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  "(P & Q) & R <-> P & (Q & R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val disj_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 ["P | True <-> True", 	"True | P <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  "P | False <-> P", 	"False | P <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  "P | P <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  "(P | Q) | R <-> P | (Q | R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val not_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
 ["~ False <-> True",	"~ True <-> False"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val imp_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
 ["(P --> False) <-> ~P",	"(P --> True) <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  "(False --> P) <-> True",	"(True --> P) <-> P", 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val iff_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
 ["(True <-> P) <-> P", 	"(P <-> True) <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  "(P <-> P) <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  "(False <-> P) <-> ~P", 	"(P <-> False) <-> ~P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val quant_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
 ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*These are NOT supplied by default!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val distrib_rews  = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
 ["~(P|Q) <-> ~P & ~Q",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val P_Imp_P_iff_T = int_prove_fun "P ==> (P <-> True)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun make_iff_T th = th RS P_Imp_P_iff_T;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val refl_iff_T = make_iff_T refl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val notFalseI = int_prove_fun "~False";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
(* Conversion into rewrite rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val not_P_imp_P_iff_F = int_prove_fun "~P ==> (P <-> False)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
fun mk_meta_eq th = case concl_of th of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
      _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
    | _ $ (Const("op =",_)$_$_) => th RS eq_reflection
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
    | _ $ (Const("Not",_)$_) => (th RS not_P_imp_P_iff_F) RS iff_reflection
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
    | _ => (make_iff_T th) RS iff_reflection;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
fun atomize th = case concl_of th of (*The operator below is Trueprop*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
      _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
    | _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
				       atomize(th RS conjunct2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    | _ $ (Const("All",_) $ _) => atomize(th RS spec)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    | _ $ (Const("True",_)) => []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    | _ $ (Const("False",_)) => []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    | _ => [th];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
fun mk_rew_rules th = map mk_meta_eq (atomize th);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
structure Induction = InductionFun(struct val spec=IFOL.spec end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val IFOL_rews =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
    imp_rews @ iff_rews @ quant_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
open Simplifier Induction;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
3
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    87
infix addcongs;
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    88
fun ss addcongs congs =
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    89
  ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    90
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val IFOL_ss = empty_ss
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
      setmksimps mk_rew_rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
      setsolver
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
      setsubgoaler asm_simp_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
      addsimps IFOL_rews
3
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    97
      addcongs [imp_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(*Classical version...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
fun prove_fun s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
    (writeln s;  prove_goal FOL.thy s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val cla_rews = map prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
 ["P | ~P", 		"~P | P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  "~ ~ P <-> P",	"(~P --> P) <-> P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val FOL_ss = IFOL_ss addsimps cla_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(*** case splitting ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val split_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  let val eq_reflection2 = prove_goal FOL.thy "x==y ==> x=y"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
                             (fn [prem] => [rewtac prem, rtac refl 1])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
      val iff_reflection2 = prove_goal FOL.thy "x==y ==> x<->y"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
                              (fn [prem] => [rewtac prem, rtac iff_refl 1])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
      val [iffD] = [eq_reflection2,iff_reflection2] RL [iffD2]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
  in fn splits => mk_case_split_tac iffD (map mk_meta_eq splits) end;