src/FOLP/FOLP.thy
changeset 17480 fd19f77dcf60
parent 3836 f1a1817659e6
child 22577 1a08fce38565
     1.1 --- a/src/FOLP/FOLP.thy	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/FOLP.thy	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -2,13 +2,88 @@
     1.4      ID:         $Id$
     1.5      Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8 -Classical First-Order Logic with Proofs
     1.9  *)
    1.10  
    1.11 -FOLP = IFOLP +
    1.12 +header {* Classical First-Order Logic with Proofs *}
    1.13 +
    1.14 +theory FOLP
    1.15 +imports IFOLP
    1.16 +uses
    1.17 +  ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
    1.18 +  ("simp.ML") ("intprover.ML") ("simpdata.ML")
    1.19 +begin
    1.20 +
    1.21  consts
    1.22    cla :: "[p=>p]=>p"
    1.23 -rules
    1.24 -  classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    1.25 +axioms
    1.26 +  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    1.27 +
    1.28 +ML {* use_legacy_bindings (the_context ()) *}
    1.29 +
    1.30 +use "FOLP_lemmas.ML"
    1.31 +
    1.32 +use "hypsubst.ML"
    1.33 +use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
    1.34 +use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
    1.35 +
    1.36 +ML {*
    1.37 +
    1.38 +(*** Applying HypsubstFun to generate hyp_subst_tac ***)
    1.39 +
    1.40 +structure Hypsubst_Data =
    1.41 +  struct
    1.42 +  (*Take apart an equality judgement; otherwise raise Match!*)
    1.43 +  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
    1.44 +
    1.45 +  val imp_intr = impI
    1.46 +
    1.47 +  (*etac rev_cut_eq moves an equality to be the last premise. *)
    1.48 +  val rev_cut_eq = prove_goal (the_context ())
    1.49 +                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    1.50 +   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    1.51 +
    1.52 +  val rev_mp = rev_mp
    1.53 +  val subst = subst
    1.54 +  val sym = sym
    1.55 +  val thin_refl = prove_goal (the_context ())
    1.56 +                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    1.57 +  end;
    1.58 +
    1.59 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.60 +open Hypsubst;
    1.61 +*}
    1.62 +
    1.63 +use "intprover.ML"
    1.64 +
    1.65 +ML {*
    1.66 +(*** Applying ClassicalFun to create a classical prover ***)
    1.67 +structure Classical_Data =
    1.68 +  struct
    1.69 +  val sizef = size_of_thm
    1.70 +  val mp = mp
    1.71 +  val not_elim = notE
    1.72 +  val swap = swap
    1.73 +  val hyp_subst_tacs=[hyp_subst_tac]
    1.74 +  end;
    1.75 +
    1.76 +structure Cla = ClassicalFun(Classical_Data);
    1.77 +open Cla;
    1.78 +
    1.79 +(*Propositional rules
    1.80 +  -- iffCE might seem better, but in the examples in ex/cla
    1.81 +     run about 7% slower than with iffE*)
    1.82 +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.83 +                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.84 +
    1.85 +(*Quantifier rules*)
    1.86 +val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    1.87 +                      addSEs [exE,ex1E] addEs [allE];
    1.88 +
    1.89 +val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
    1.90 +                          addSEs [exE,ex1E] addEs [all_dupE];
    1.91 +
    1.92 +*}
    1.93 +
    1.94 +use "simpdata.ML"
    1.95 +
    1.96  end