src/FOL/simpdata.ML
author lcp
Fri May 13 11:25:55 1994 +0200 (1994-05-13)
changeset 371 3a853818f1d2
parent 282 731b27c90d2f
child 394 432bb9995893
permissions -rw-r--r--
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
simplifier can rewrite premises, it can generate the premise False."
clasohm@0
     1
(*  Title: 	FOL/simpdata
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@282
     4
    Copyright   1994  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Simplification data for FOL
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*** Rewrite rules ***)
clasohm@0
    10
clasohm@0
    11
fun int_prove_fun s = 
lcp@282
    12
 (writeln s;  
lcp@282
    13
  prove_goal IFOL.thy s
lcp@282
    14
   (fn prems => [ (cut_facts_tac prems 1), 
lcp@282
    15
		  (Int.fast_tac 1) ]));
clasohm@0
    16
clasohm@0
    17
val conj_rews = map int_prove_fun
lcp@282
    18
 ["P & True <-> P", 	 "True & P <-> P",
clasohm@0
    19
  "P & False <-> False", "False & P <-> False",
clasohm@0
    20
  "P & P <-> P",
lcp@282
    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@0
    25
 ["P | True <-> True", 	"True | P <-> True",
clasohm@0
    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
lcp@282
    31
 ["~(P|Q)  <-> ~P & ~Q",
lcp@282
    32
  "~ False <-> True",	"~ True <-> False"];
clasohm@0
    33
clasohm@0
    34
val imp_rews = map int_prove_fun
clasohm@0
    35
 ["(P --> False) <-> ~P",	"(P --> True) <-> True",
clasohm@0
    36
  "(False --> P) <-> True",	"(True --> P) <-> P", 
clasohm@0
    37
  "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];
clasohm@0
    38
clasohm@0
    39
val iff_rews = map int_prove_fun
clasohm@0
    40
 ["(True <-> P) <-> P", 	"(P <-> True) <-> P",
clasohm@0
    41
  "(P <-> P) <-> True",
clasohm@0
    42
  "(False <-> P) <-> ~P", 	"(P <-> False) <-> ~P"];
clasohm@0
    43
clasohm@0
    44
val quant_rews = map int_prove_fun
clasohm@0
    45
 ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
clasohm@0
    46
clasohm@0
    47
(*These are NOT supplied by default!*)
clasohm@0
    48
val distrib_rews  = map int_prove_fun
lcp@282
    49
 ["P & (Q | R) <-> P&Q | P&R", 
lcp@282
    50
  "(Q | R) & P <-> Q&P | R&P",
clasohm@0
    51
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
clasohm@0
    52
lcp@282
    53
(** Conversion into rewrite rules **)
clasohm@0
    54
nipkow@53
    55
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
nipkow@53
    56
lcp@282
    57
(*Make atomic rewrite rules*)
lcp@282
    58
fun atomize th = case concl_of th of 
lcp@282
    59
    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) @
lcp@282
    60
				       atomize(th RS conjunct2)
lcp@282
    61
  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
lcp@282
    62
  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
lcp@282
    63
  | _ $ (Const("True",_))           => []
lcp@282
    64
  | _ $ (Const("False",_))          => []
lcp@282
    65
  | _                               => [th];
lcp@282
    66
lcp@282
    67
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
lcp@282
    68
val iff_reflection_F = P_iff_F RS iff_reflection;
lcp@282
    69
lcp@282
    70
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
lcp@282
    71
val iff_reflection_T = P_iff_T RS iff_reflection;
lcp@282
    72
lcp@282
    73
(*Make meta-equalities.  The operator below is Trueprop*)
lcp@282
    74
fun mk_meta_eq th = case concl_of th of
lcp@282
    75
    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
lcp@282
    76
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
lcp@282
    77
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
lcp@282
    78
  | _                           => th RS iff_reflection_T;
clasohm@0
    79
clasohm@0
    80
structure Induction = InductionFun(struct val spec=IFOL.spec end);
clasohm@0
    81
clasohm@0
    82
open Simplifier Induction;
clasohm@0
    83
nipkow@3
    84
infix addcongs;
nipkow@3
    85
fun ss addcongs congs =
lcp@282
    86
    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
lcp@282
    87
lcp@282
    88
val IFOL_rews =
lcp@282
    89
   [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
lcp@282
    90
    imp_rews @ iff_rews @ quant_rews;
nipkow@3
    91
lcp@282
    92
val notFalseI = int_prove_fun "~False";
lcp@282
    93
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
lcp@282
    94
lcp@282
    95
val IFOL_ss = 
lcp@282
    96
  empty_ss 
lcp@282
    97
  setmksimps (map mk_meta_eq o atomize o gen_all)
lcp@371
    98
  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
lcp@371
    99
	                  ORELSE' assume_tac
lcp@371
   100
	                  ORELSE' etac FalseE)
lcp@282
   101
  setsubgoaler asm_simp_tac
lcp@282
   102
  addsimps IFOL_rews
lcp@282
   103
  addcongs [imp_cong];
clasohm@0
   104
clasohm@0
   105
(*Classical version...*)
clasohm@0
   106
fun prove_fun s = 
lcp@282
   107
 (writeln s;  
lcp@282
   108
  prove_goal FOL.thy s
lcp@282
   109
   (fn prems => [ (cut_facts_tac prems 1), 
lcp@282
   110
		  (Cla.fast_tac FOL_cs 1) ]));
clasohm@0
   111
val cla_rews = map prove_fun
lcp@282
   112
 ["~(P&Q)  <-> ~P | ~Q",
lcp@282
   113
  "P | ~P", 		"~P | P",
clasohm@0
   114
  "~ ~ P <-> P",	"(~P --> P) <-> P"];
clasohm@0
   115
clasohm@0
   116
val FOL_ss = IFOL_ss addsimps cla_rews;
clasohm@0
   117
clasohm@0
   118
(*** case splitting ***)
clasohm@0
   119
lcp@282
   120
val meta_iffD = 
lcp@282
   121
    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
lcp@282
   122
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
lcp@282
   123
lcp@282
   124
fun split_tac splits =
lcp@282
   125
    mk_case_split_tac meta_iffD (map mk_meta_eq splits);