src/FOL/simpdata.ML
author oheimb
Wed, 25 Feb 1998 20:25:27 +0100
changeset 4652 d24cca140eeb
parent 4649 89ad3eb863a1
child 4669 06f3c56dcba8
permissions -rw-r--r--
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
     1
(*  Title:      FOL/simpdata
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
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), 
2601
b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents: 2469
diff changeset
    15
                  (IntPr.fast_tac 1) ]));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    17
val conj_simps = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    18
 ["P & True <-> P",      "True & P <-> P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  "P & False <-> False", "False & P <-> False",
2801
56948cb1a1f9 Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
nipkow
parents: 2727
diff changeset
    20
  "P & P <-> P", "P & P & Q <-> P & Q",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
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
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    24
val disj_simps = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    25
 ["P | True <-> True",  "True | P <-> True",
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    26
  "P | False <-> P",    "False | P <-> P",
2801
56948cb1a1f9 Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
nipkow
parents: 2727
diff changeset
    27
  "P | P <-> P", "P | P | Q <-> P | Q",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  "(P | Q) | R <-> P | (Q | R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    30
val not_simps = map int_prove_fun
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    31
 ["~(P|Q)  <-> ~P & ~Q",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    32
  "~ False <-> True",   "~ True <-> False"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    34
val imp_simps = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    35
 ["(P --> False) <-> ~P",       "(P --> True) <-> True",
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    36
  "(False --> P) <-> True",     "(True --> P) <-> P", 
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    37
  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    39
val iff_simps = map int_prove_fun
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    40
 ["(True <-> P) <-> P",         "(P <-> True) <-> P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  "(P <-> P) <-> True",
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    42
  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    44
(*The x=t versions are needed for the simplification procedures*)
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    45
val quant_simps = map int_prove_fun
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    46
 ["(ALL x. P) <-> P",   
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    47
  "(ALL x. x=t --> P(x)) <-> P(t)",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    48
  "(ALL x. t=x --> P(x)) <-> P(t)",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    49
  "(EX x. P) <-> P",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    50
  "(EX x. x=t & P(x)) <-> P(t)", 
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
    51
  "(EX x. t=x & P(x)) <-> P(t)"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
(*These are NOT supplied by default!*)
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
    54
val distrib_simps  = map int_prove_fun
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    55
 ["P & (Q | R) <-> P&Q | P&R", 
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    56
  "(Q | R) & P <-> Q&P | R&P",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    59
(** Conversion into rewrite rules **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
53
f8f37a9a31dc Added gen_all to simpdata.ML.
nipkow
parents: 3
diff changeset
    61
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
    62
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    63
(*Make atomic rewrite rules*)
429
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    64
fun atomize r =
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    65
  case concl_of r of
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    66
    Const("Trueprop",_) $ p =>
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    67
      (case p of
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    68
         Const("op -->",_)$_$_ => atomize(r RS mp)
429
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    69
       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    70
                                  atomize(r RS conjunct2)
429
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    71
       | Const("All",_)$_      => atomize(r RS spec)
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    72
       | Const("True",_)       => []    (*True is DELETED*)
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    73
       | Const("False",_)      => []    (*should False do something?*)
429
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    74
       | _                     => [r])
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    75
  | _ => [r];
888bbb4119f8 atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents: 394
diff changeset
    76
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    77
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    78
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    79
val iff_reflection_F = P_iff_F RS iff_reflection;
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    80
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    81
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    82
val iff_reflection_T = P_iff_T RS iff_reflection;
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    83
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    84
(*Make meta-equalities.  The operator below is Trueprop*)
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    85
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
    86
    Const("==",_)$_$_           => th
432bb9995893 Modified mk_meta_eq to leave meta-equlities on unchanged.
nipkow
parents: 371
diff changeset
    87
  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    88
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    89
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    90
  | _                           => th RS iff_reflection_T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
981
864370666a24 Defined addss to perform simplification in a claset.
lcp
parents: 942
diff changeset
    92
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
    93
(*** Classical laws ***)
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    94
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
fun prove_fun s = 
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    96
 (writeln s;  
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    97
  prove_goal FOL.thy s
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
    98
   (fn prems => [ (cut_facts_tac prems 1), 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1088
diff changeset
    99
                  (Cla.fast_tac FOL_cs 1) ]));
745
45a789407806 added blank line
lcp
parents: 429
diff changeset
   100
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   101
(*Avoids duplication of subgoals after expand_if, when the true and false 
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   102
  cases boil down to the same thing.*) 
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   103
val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   104
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   105
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   106
(*** Miniscoping: pushing quantifiers in
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   107
     We do NOT distribute of ALL over &, or dually that of EX over |
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   108
     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   109
     show that this step can increase proof length!
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   110
***)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   111
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   112
(*existential miniscoping*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   113
val int_ex_simps = map int_prove_fun 
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   114
		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   115
		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   116
		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   117
		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   118
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   119
(*classical rules*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   120
val cla_ex_simps = map prove_fun 
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   121
                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   122
		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   124
val ex_simps = int_ex_simps @ cla_ex_simps;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   125
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   126
(*universal miniscoping*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   127
val int_all_simps = map int_prove_fun
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   128
		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   129
		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   130
		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   131
		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   132
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   133
(*classical rules*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   134
val cla_all_simps = map prove_fun
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   135
                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   136
		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   137
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   138
val all_simps = int_all_simps @ cla_all_simps;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   139
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   140
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   141
(*** Named rewrite rules proved for IFOL ***)
1953
832ccc1dba95 Introduction of miniscoping for FOL
paulson
parents: 1914
diff changeset
   142
1914
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   143
fun int_prove nm thm  = qed_goal nm IFOL.thy thm
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   144
    (fn prems => [ (cut_facts_tac prems 1), 
2601
b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents: 2469
diff changeset
   145
                   (IntPr.fast_tac 1) ]);
1914
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   146
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   147
fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
1914
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   148
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   149
int_prove "conj_commute" "P&Q <-> Q&P";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   150
int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   151
val conj_comms = [conj_commute, conj_left_commute];
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   152
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   153
int_prove "disj_commute" "P|Q <-> Q|P";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   154
int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   155
val disj_comms = [disj_commute, disj_left_commute];
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   156
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   157
int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   158
int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   159
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   160
int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   161
int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   162
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   163
int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   164
int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   165
int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   166
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   167
prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   168
prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   169
1914
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   170
int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   171
prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   172
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   173
prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   174
3835
9a5a4e123859 fixed dots;
wenzelm
parents: 3610
diff changeset
   175
prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
9a5a4e123859 fixed dots;
wenzelm
parents: 3610
diff changeset
   176
prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
9a5a4e123859 fixed dots;
wenzelm
parents: 3610
diff changeset
   177
int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
1914
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   178
int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   179
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   180
int_prove "ex_disj_distrib"
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   181
    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   182
int_prove "all_conj_distrib"
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   183
    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   184
86b095835de9 Added a lot of basic laws, from HOL/simpdata
paulson
parents: 1722
diff changeset
   185
1088
fc4fb6e8a636 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents: 981
diff changeset
   186
(*Used in ZF, perhaps elsewhere?*)
fc4fb6e8a636 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents: 981
diff changeset
   187
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
fc4fb6e8a636 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents: 981
diff changeset
   188
  (fn [prem] => [rewtac prem, rtac refl 1]);
fc4fb6e8a636 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents: 981
diff changeset
   189
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   190
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   191
open Simplifier;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   192
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   193
(** make simplification procedures for quantifier elimination **)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   194
structure Quantifier1 = Quantifier1Fun(
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   195
struct
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   196
  (*abstract syntax*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   197
  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   198
    | dest_eq _ = None;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   199
  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   200
    | dest_conj _ = None;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   201
  val conj = FOLogic.conj
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   202
  val imp  = FOLogic.imp
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   203
  (*rules*)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   204
  val iff_reflection = iff_reflection
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   205
  val iffI = iffI
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   206
  val sym  = sym
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   207
  val conjI= conjI
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   208
  val conjE= conjE
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   209
  val impI = impI
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   210
  val impE = impE
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   211
  val mp   = mp
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   212
  val exI  = exI
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   213
  val exE  = exE
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   214
  val allI = allI
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   215
  val allE = allE
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   216
end);
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   217
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   218
local
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   219
val ex_pattern =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   220
  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   221
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   222
val all_pattern =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   223
  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   224
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   225
in
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   226
val defEX_regroup =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   227
  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   228
val defALL_regroup =
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   229
  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   230
end;
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   231
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   232
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   233
(*** Case splitting ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
1088
fc4fb6e8a636 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents: 981
diff changeset
   235
qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
756
e0e5c1581e4c added qed_goal for meta_iffD
clasohm
parents: 745
diff changeset
   236
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
282
731b27c90d2f FOL/simpdata: tidied
lcp
parents: 215
diff changeset
   237
942
d9edeb96b51c Enforced partial evaluation of mk_case_split_tac.
nipkow
parents: 784
diff changeset
   238
local val mktac = mk_case_split_tac meta_iffD
d9edeb96b51c Enforced partial evaluation of mk_case_split_tac.
nipkow
parents: 784
diff changeset
   239
in
d9edeb96b51c Enforced partial evaluation of mk_case_split_tac.
nipkow
parents: 784
diff changeset
   240
fun split_tac splits = mktac (map mk_meta_eq splits)
d9edeb96b51c Enforced partial evaluation of mk_case_split_tac.
nipkow
parents: 784
diff changeset
   241
end;
1722
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   242
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   243
local val mktac = mk_case_split_inside_tac meta_iffD
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   244
in
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   245
fun split_inside_tac splits = mktac (map mk_meta_eq splits)
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   246
end;
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   247
4203
ca73de799b73 renamed split_prem_tac to split_asm_tac
oheimb
parents: 4189
diff changeset
   248
val split_asm_tac = mk_case_split_asm_tac split_tac 
ca73de799b73 renamed split_prem_tac to split_asm_tac
oheimb
parents: 4189
diff changeset
   249
			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
1722
bb326972ede6 Added split_inside_tac.
berghofe
parents: 1459
diff changeset
   250
4325
e72cba5af6c5 addsplits now in FOL, ZF too
paulson
parents: 4203
diff changeset
   251
e72cba5af6c5 addsplits now in FOL, ZF too
paulson
parents: 4203
diff changeset
   252
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   253
(*** Standard simpsets ***)
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   254
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   255
structure Induction = InductionFun(struct val spec=IFOL.spec end);
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   256
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   257
open Induction;
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   258
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   259
(*Add congruence rules for = or <-> (instead of ==) *)
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   260
infix 4 addcongs delcongs;
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   261
fun ss addcongs congs =
3566
c9c351374651 standard congs;
wenzelm
parents: 3537
diff changeset
   262
        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   263
fun ss delcongs congs =
3566
c9c351374651 standard congs;
wenzelm
parents: 3537
diff changeset
   264
        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 2074
diff changeset
   265
4094
9e501199ec01 adapted to new implicit simpset;
wenzelm
parents: 3910
diff changeset
   266
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
9e501199ec01 adapted to new implicit simpset;
wenzelm
parents: 3910
diff changeset
   267
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   268
4325
e72cba5af6c5 addsplits now in FOL, ZF too
paulson
parents: 4203
diff changeset
   269
infix 4 addsplits;
e72cba5af6c5 addsplits now in FOL, ZF too
paulson
parents: 4203
diff changeset
   270
fun ss addsplits splits = ss addloop (split_tac splits);
e72cba5af6c5 addsplits now in FOL, ZF too
paulson
parents: 4203
diff changeset
   271
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   272
val IFOL_simps =
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   273
   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   274
    imp_simps @ iff_simps @ quant_simps;
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   275
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   276
val notFalseI = int_prove_fun "~False";
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   277
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   278
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   279
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   280
				 atac, etac FalseE];
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   281
(*No premature instantiation of variables during simplification*)
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   282
fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   283
				 eq_assume_tac, ematch_tac [FalseE]];
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   284
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   285
(*No simprules, but basic infastructure for simplification*)
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   286
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   287
                            addsimprocs [defALL_regroup,defEX_regroup]
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   288
			    setSSolver   safe_solver
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   289
			    setSolver  unsafe_solver
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   290
			    setmksimps (map mk_meta_eq o atomize o gen_all);
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   291
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   292
(*intuitionistic simprules only*)
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   293
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   294
			   addcongs [imp_cong];
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   295
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   296
val cla_simps = 
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   297
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   298
     not_all, not_ex, cases_simp] @
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   299
    map prove_fun
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   300
     ["~(P&Q)  <-> ~P | ~Q",
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   301
      "P | ~P",             "~P | P",
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   302
      "~ ~ P <-> P",        "(~P --> P) <-> P",
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   303
      "(~P <-> ~Q) <-> (P<->Q)"];
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   304
3910
1cc9b8ab161c New simprules imp_disj1,2 and some comments
paulson
parents: 3835
diff changeset
   305
(*classical simprules too*)
4349
50403e5a44c0 Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents: 4325
diff changeset
   306
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
2074
30a65172e003 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents: 2065
diff changeset
   307
4094
9e501199ec01 adapted to new implicit simpset;
wenzelm
parents: 3910
diff changeset
   308
simpset_ref() := FOL_ss;
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   309
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   310
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   311
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   312
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   313
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   314
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   315
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   316
(*** Integration of simplifier with classical reasoner ***)
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   317
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   318
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   319
   fails if there is no equaliy or if an equality is already at the front *)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   320
local
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   321
  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   322
    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   323
    | is_eq _ = false;
4188
1025a27b08f9 changed libraray function find to find_index_eq, currying it
oheimb
parents: 4094
diff changeset
   324
  val find_eq = find_index is_eq;
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   325
in
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   326
val rot_eq_tac = 
4188
1025a27b08f9 changed libraray function find to find_index_eq, currying it
oheimb
parents: 4094
diff changeset
   327
     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
1025a27b08f9 changed libraray function find to find_index_eq, currying it
oheimb
parents: 4094
diff changeset
   328
		if n>0 then rotate_tac n i else no_tac end)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 3206
diff changeset
   329
end;
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   330
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   331
use "$ISABELLE_HOME/src/Provers/clasimp.ML";
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents: 4649
diff changeset
   332
open Clasimp;
2633
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   333
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   334
val FOL_css = (FOL_cs, FOL_ss);
37c0b5a7ee5d added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents: 2601
diff changeset
   335