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