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 |
|
393
|
14 |
init_thy_reader();
|
72
|
15 |
|
0
|
16 |
print_depth 1;
|
|
17 |
|
|
18 |
use "../Provers/splitter.ML";
|
|
19 |
use "../Provers/ind.ML";
|
1004
|
20 |
use "../Provers/hypsubst.ML";
|
|
21 |
use "../Provers/classical.ML";
|
2866
|
22 |
use "../Provers/blast.ML";
|
0
|
23 |
|
2469
|
24 |
use_thy "IFOL";
|
0
|
25 |
|
2866
|
26 |
(** Applying HypsubstFun to generate hyp_subst_tac **)
|
0
|
27 |
structure Hypsubst_Data =
|
|
28 |
struct
|
1004
|
29 |
structure Simplifier = Simplifier
|
|
30 |
(*Take apart an equality judgement; otherwise raise Match!*)
|
|
31 |
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u)
|
|
32 |
val eq_reflection = eq_reflection
|
0
|
33 |
val imp_intr = impI
|
|
34 |
val rev_mp = rev_mp
|
|
35 |
val subst = subst
|
|
36 |
val sym = sym
|
|
37 |
end;
|
|
38 |
|
|
39 |
structure Hypsubst = HypsubstFun(Hypsubst_Data);
|
|
40 |
open Hypsubst;
|
|
41 |
|
2469
|
42 |
|
97
|
43 |
use "intprover.ML";
|
0
|
44 |
|
2469
|
45 |
use_thy "FOL";
|
0
|
46 |
|
1523
|
47 |
qed_goal "ex1_functional" FOL.thy
|
666
|
48 |
"!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
|
731
|
49 |
(fn _ => [ (deepen_tac FOL_cs 0 1) ]);
|
0
|
50 |
|
|
51 |
|
2237
|
52 |
init_pps ();
|
0
|
53 |
print_depth 8;
|
|
54 |
|
1459
|
55 |
val FOL_build_completed = (); (*indicate successful build*)
|