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