src/FOLP/FOLP.thy
changeset 17480 fd19f77dcf60
parent 3836 f1a1817659e6
child 22577 1a08fce38565
equal deleted inserted replaced
17479:68a7acb5f22e 17480:fd19f77dcf60
     1 (*  Title:      FOLP/FOLP.thy
     1 (*  Title:      FOLP/FOLP.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
       
     6 Classical First-Order Logic with Proofs
       
     7 *)
     5 *)
     8 
     6 
     9 FOLP = IFOLP +
     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 
    10 consts
    16 consts
    11   cla :: "[p=>p]=>p"
    17   cla :: "[p=>p]=>p"
    12 rules
    18 axioms
    13   classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    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 
    14 end
    89 end