src/FOLP/FOLP.thy
author wenzelm
Sun Sep 18 14:25:48 2005 +0200 (2005-09-18)
changeset 17480 fd19f77dcf60
parent 3836 f1a1817659e6
child 22577 1a08fce38565
permissions -rw-r--r--
converted to Isar theory format;
clasohm@1477
     1
(*  Title:      FOLP/FOLP.thy
lcp@1142
     2
    ID:         $Id$
clasohm@1477
     3
    Author:     Martin D Coen, Cambridge University Computer Laboratory
lcp@1142
     4
    Copyright   1992  University of Cambridge
lcp@1142
     5
*)
lcp@1142
     6
wenzelm@17480
     7
header {* Classical First-Order Logic with Proofs *}
wenzelm@17480
     8
wenzelm@17480
     9
theory FOLP
wenzelm@17480
    10
imports IFOLP
wenzelm@17480
    11
uses
wenzelm@17480
    12
  ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
wenzelm@17480
    13
  ("simp.ML") ("intprover.ML") ("simpdata.ML")
wenzelm@17480
    14
begin
wenzelm@17480
    15
clasohm@0
    16
consts
clasohm@0
    17
  cla :: "[p=>p]=>p"
wenzelm@17480
    18
axioms
wenzelm@17480
    19
  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
wenzelm@17480
    20
wenzelm@17480
    21
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17480
    22
wenzelm@17480
    23
use "FOLP_lemmas.ML"
wenzelm@17480
    24
wenzelm@17480
    25
use "hypsubst.ML"
wenzelm@17480
    26
use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
wenzelm@17480
    27
use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
wenzelm@17480
    28
wenzelm@17480
    29
ML {*
wenzelm@17480
    30
wenzelm@17480
    31
(*** Applying HypsubstFun to generate hyp_subst_tac ***)
wenzelm@17480
    32
wenzelm@17480
    33
structure Hypsubst_Data =
wenzelm@17480
    34
  struct
wenzelm@17480
    35
  (*Take apart an equality judgement; otherwise raise Match!*)
wenzelm@17480
    36
  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
wenzelm@17480
    37
wenzelm@17480
    38
  val imp_intr = impI
wenzelm@17480
    39
wenzelm@17480
    40
  (*etac rev_cut_eq moves an equality to be the last premise. *)
wenzelm@17480
    41
  val rev_cut_eq = prove_goal (the_context ())
wenzelm@17480
    42
                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
wenzelm@17480
    43
   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
wenzelm@17480
    44
wenzelm@17480
    45
  val rev_mp = rev_mp
wenzelm@17480
    46
  val subst = subst
wenzelm@17480
    47
  val sym = sym
wenzelm@17480
    48
  val thin_refl = prove_goal (the_context ())
wenzelm@17480
    49
                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
wenzelm@17480
    50
  end;
wenzelm@17480
    51
wenzelm@17480
    52
structure Hypsubst = HypsubstFun(Hypsubst_Data);
wenzelm@17480
    53
open Hypsubst;
wenzelm@17480
    54
*}
wenzelm@17480
    55
wenzelm@17480
    56
use "intprover.ML"
wenzelm@17480
    57
wenzelm@17480
    58
ML {*
wenzelm@17480
    59
(*** Applying ClassicalFun to create a classical prover ***)
wenzelm@17480
    60
structure Classical_Data =
wenzelm@17480
    61
  struct
wenzelm@17480
    62
  val sizef = size_of_thm
wenzelm@17480
    63
  val mp = mp
wenzelm@17480
    64
  val not_elim = notE
wenzelm@17480
    65
  val swap = swap
wenzelm@17480
    66
  val hyp_subst_tacs=[hyp_subst_tac]
wenzelm@17480
    67
  end;
wenzelm@17480
    68
wenzelm@17480
    69
structure Cla = ClassicalFun(Classical_Data);
wenzelm@17480
    70
open Cla;
wenzelm@17480
    71
wenzelm@17480
    72
(*Propositional rules
wenzelm@17480
    73
  -- iffCE might seem better, but in the examples in ex/cla
wenzelm@17480
    74
     run about 7% slower than with iffE*)
wenzelm@17480
    75
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
wenzelm@17480
    76
                       addSEs [conjE,disjE,impCE,FalseE,iffE];
wenzelm@17480
    77
wenzelm@17480
    78
(*Quantifier rules*)
wenzelm@17480
    79
val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
wenzelm@17480
    80
                      addSEs [exE,ex1E] addEs [allE];
wenzelm@17480
    81
wenzelm@17480
    82
val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
wenzelm@17480
    83
                          addSEs [exE,ex1E] addEs [all_dupE];
wenzelm@17480
    84
wenzelm@17480
    85
*}
wenzelm@17480
    86
wenzelm@17480
    87
use "simpdata.ML"
wenzelm@17480
    88
clasohm@0
    89
end