src/FOL/simpdata.ML
author lcp
Fri, 25 Nov 1994 00:02:37 +0100
changeset 745 45a789407806
parent 429 888bbb4119f8
child 756 e0e5c1581e4c
permissions -rw-r--r--
added blank line
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
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
     4
    Copyright   1994  University of Cambridge
0
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 = 
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    12
 (writeln s;  
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    13
  prove_goal IFOL.thy s
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    14
   (fn prems => [ (cut_facts_tac prems 1), 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    15
		  (Int.fast_tac 1) ]));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val conj_rews = map int_prove_fun
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
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",
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
 ["P | True <-> True", 	"True | P <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  "P | False <-> P", 	"False | P <-> P",
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
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    31
 ["~(P|Q)  <-> ~P & ~Q",
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    32
  "~ False <-> True",	"~ True <-> False"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val imp_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
 ["(P --> False) <-> ~P",	"(P --> True) <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  "(False --> P) <-> True",	"(True --> P) <-> P", 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val iff_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
 ["(True <-> P) <-> P", 	"(P <-> True) <-> P",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  "(P <-> P) <-> True",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  "(False <-> P) <-> ~P", 	"(P <-> False) <-> ~P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
val quant_rews = map int_prove_fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
 ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*These are NOT supplied by default!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val distrib_rews  = map int_prove_fun
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    49
 ["P & (Q | R) <-> P&Q | P&R", 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    50
  "(Q | R) & P <-> Q&P | R&P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    53
(** Conversion into rewrite rules **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
53
f8f37a9a31dc Added gen_all to simpdata.ML.
nipkow
parents: 3
diff changeset
    55
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
f8f37a9a31dc Added gen_all to simpdata.ML.
nipkow
parents: 3
diff changeset
    56
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    57
(*Make atomic rewrite rules*)
429
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    58
fun atomize r =
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    59
  case concl_of r of
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    60
    Const("Trueprop",_) $ p =>
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    61
      (case p of
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    62
	 Const("op -->",_)$_$_ => atomize(r RS mp)
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    63
       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    64
	  		          atomize(r RS conjunct2)
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    65
       | Const("All",_)$_      => atomize(r RS spec)
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    66
       | Const("True",_)       => []	(*True is DELETED*)
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    67
       | Const("False",_)      => []	(*should False do something?*)
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    68
       | _                     => [r])
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    69
  | _ => [r];
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    70
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    71
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    72
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    73
val iff_reflection_F = P_iff_F RS iff_reflection;
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    74
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    75
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    76
val iff_reflection_T = P_iff_T RS iff_reflection;
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    77
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    78
(*Make meta-equalities.  The operator below is Trueprop*)
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    79
fun mk_meta_eq th = case concl_of th of
394
432bb9995893 Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents: 371
diff changeset
    80
    Const("==",_)$_$_           => th
432bb9995893 Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents: 371
diff changeset
    81
  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    82
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    83
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    84
  | _                           => th RS iff_reflection_T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
structure Induction = InductionFun(struct val spec=IFOL.spec end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
open Simplifier Induction;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
3
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    90
infix addcongs;
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    91
fun ss addcongs congs =
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    92
    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    93
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    94
val IFOL_rews =
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    95
   [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    96
    imp_rews @ iff_rews @ quant_rews;
3
5f77582e3a89 defined local addcongs
nipkow
parents: 0
diff changeset
    97
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    98
val notFalseI = int_prove_fun "~False";
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    99
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   100
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   101
val IFOL_ss = 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   102
  empty_ss 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   103
  setmksimps (map mk_meta_eq o atomize o gen_all)
371
3a853818f1d2 FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents: 282
diff changeset
   104
  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
3a853818f1d2 FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents: 282
diff changeset
   105
	                  ORELSE' assume_tac
3a853818f1d2 FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents: 282
diff changeset
   106
	                  ORELSE' etac FalseE)
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   107
  setsubgoaler asm_simp_tac
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   108
  addsimps IFOL_rews
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   109
  addcongs [imp_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
(*Classical version...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
fun prove_fun s = 
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   113
 (writeln s;  
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   114
  prove_goal FOL.thy s
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   115
   (fn prems => [ (cut_facts_tac prems 1), 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   116
		  (Cla.fast_tac FOL_cs 1) ]));
745
45a789407806 added blank line
lcp
parents: 429
diff changeset
   117
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val cla_rews = map prove_fun
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   119
 ["~(P&Q)  <-> ~P | ~Q",
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   120
  "P | ~P", 		"~P | P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
  "~ ~ P <-> P",	"(~P --> P) <-> P"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
val FOL_ss = IFOL_ss addsimps cla_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*** case splitting ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   127
val meta_iffD = 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   128
    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   129
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   130
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   131
fun split_tac splits =
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   132
    mk_case_split_tac meta_iffD (map mk_meta_eq splits);