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.84 +
1.85 +(*Quantifier rules*)