src/FOL/ROOT.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5310 3e14d6d66dab
child 6260 a8010d459ef7
permissions -rw-r--r--
made tutorial first;
clasohm@1459
     1
(*  Title:      FOL/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Adds First-Order Logic to a database containing pure Isabelle. 
clasohm@0
     7
Should be executed in the subdirectory FOL.
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
val banner = "First-Order Logic with Natural Deduction";
clasohm@0
    11
clasohm@0
    12
writeln banner;
clasohm@0
    13
clasohm@0
    14
print_depth 1;  
clasohm@0
    15
wenzelm@4222
    16
use "$ISABELLE_HOME/src/Provers/simplifier.ML";
wenzelm@4222
    17
use "$ISABELLE_HOME/src/Provers/splitter.ML";
wenzelm@4222
    18
use "$ISABELLE_HOME/src/Provers/ind.ML";
wenzelm@4222
    19
use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
wenzelm@4222
    20
use "$ISABELLE_HOME/src/Provers/classical.ML";
wenzelm@4222
    21
use "$ISABELLE_HOME/src/Provers/blast.ML";
wenzelm@5219
    22
use "$ISABELLE_HOME/src/Provers/clasimp.ML";
paulson@4349
    23
use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
clasohm@0
    24
paulson@2469
    25
use_thy "IFOL";
paulson@4349
    26
use "fologic.ML";
clasohm@0
    27
paulson@2866
    28
(** Applying HypsubstFun to generate hyp_subst_tac **)
clasohm@0
    29
structure Hypsubst_Data =
clasohm@0
    30
  struct
lcp@1004
    31
  structure Simplifier = Simplifier
paulson@4466
    32
    (*These destructors  Match!*)
paulson@4466
    33
  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
paulson@4466
    34
  val dest_Trueprop = FOLogic.dest_Trueprop
paulson@4466
    35
  val dest_imp = FOLogic.dest_imp
lcp@1004
    36
  val eq_reflection = eq_reflection
clasohm@0
    37
  val imp_intr = impI
clasohm@0
    38
  val rev_mp = rev_mp
clasohm@0
    39
  val subst = subst
clasohm@0
    40
  val sym = sym
oheimb@4223
    41
  val thin_refl = prove_goal IFOL.thy 
oheimb@4223
    42
		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
clasohm@0
    43
  end;
clasohm@0
    44
clasohm@0
    45
structure Hypsubst = HypsubstFun(Hypsubst_Data);
clasohm@0
    46
open Hypsubst;
clasohm@0
    47
paulson@2469
    48
clasohm@97
    49
use "intprover.ML";
clasohm@0
    50
paulson@2469
    51
use_thy "FOL";
clasohm@0
    52
wenzelm@4096
    53
use "cladata.ML";
wenzelm@4096
    54
use "simpdata.ML";
wenzelm@4096
    55
paulson@1523
    56
qed_goal "ex1_functional" FOL.thy
lcp@666
    57
    "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
paulson@5310
    58
 (fn _ => [ (Blast_tac 1) ]);
clasohm@0
    59
clasohm@0
    60
clasohm@0
    61
print_depth 8;
clasohm@0
    62
clasohm@1459
    63
val FOL_build_completed = ();   (*indicate successful build*)