author | paulson |
Wed, 03 Dec 1997 10:48:16 +0100 | |
changeset 4349 | 50403e5a44c0 |
parent 4223 | f60e3d2c81d3 |
child 4466 | 305390f23734 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/ROOT |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Adds First-Order Logic to a database containing pure Isabelle. |
|
7 |
Should be executed in the subdirectory FOL. |
|
8 |
*) |
|
9 |
||
10 |
val banner = "First-Order Logic with Natural Deduction"; |
|
11 |
||
12 |
writeln banner; |
|
13 |
||
14 |
print_depth 1; |
|
15 |
||
4222 | 16 |
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; |
17 |
use "$ISABELLE_HOME/src/Provers/splitter.ML"; |
|
18 |
use "$ISABELLE_HOME/src/Provers/ind.ML"; |
|
19 |
use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; |
|
20 |
use "$ISABELLE_HOME/src/Provers/classical.ML"; |
|
21 |
use "$ISABELLE_HOME/src/Provers/blast.ML"; |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4223
diff
changeset
|
22 |
use "$ISABELLE_HOME/src/Provers/quantifier1.ML"; |
0 | 23 |
|
2469 | 24 |
use_thy "IFOL"; |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
4223
diff
changeset
|
25 |
use "fologic.ML"; |
0 | 26 |
|
2866 | 27 |
(** Applying HypsubstFun to generate hyp_subst_tac **) |
0 | 28 |
structure Hypsubst_Data = |
29 |
struct |
|
1004 | 30 |
structure Simplifier = Simplifier |
31 |
(*Take apart an equality judgement; otherwise raise Match!*) |
|
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4096
diff
changeset
|
32 |
fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = |
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4096
diff
changeset
|
33 |
(t, u, domain_type T) |
1004 | 34 |
val eq_reflection = eq_reflection |
0 | 35 |
val imp_intr = impI |
36 |
val rev_mp = rev_mp |
|
37 |
val subst = subst |
|
38 |
val sym = sym |
|
4223 | 39 |
val thin_refl = prove_goal IFOL.thy |
40 |
"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); |
|
0 | 41 |
end; |
42 |
||
43 |
structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
44 |
open Hypsubst; |
|
45 |
||
2469 | 46 |
|
97 | 47 |
use "intprover.ML"; |
0 | 48 |
|
2469 | 49 |
use_thy "FOL"; |
0 | 50 |
|
4096 | 51 |
use "cladata.ML"; |
52 |
use "simpdata.ML"; |
|
53 |
||
1523 | 54 |
qed_goal "ex1_functional" FOL.thy |
666 | 55 |
"!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" |
731 | 56 |
(fn _ => [ (deepen_tac FOL_cs 0 1) ]); |
0 | 57 |
|
58 |
||
59 |
print_depth 8; |
|
60 |
||
1459 | 61 |
val FOL_build_completed = (); (*indicate successful build*) |